Social Choice in mathlib

Stream: general

[Andrew Souther]

I would like to start a conversation about PRing my work on Social Choice Theory in Lean. Right now, my repo has two main files:

1. In the basic file, I have been slowly formalizing the first chapter of Collective Choice and Social Welfare by Amartya Sen. I have just been working through and formalizing each definition and lemma as they come, without much thought yet towards building a user-friendly library.

2. In the arrows_theorem file, I have formalized a proof of Arrow's Impossibility Theorem.

Some maintainers have expressed interest in getting this work on mathlib. What should a PR look like for this work? Should I start with Arrow's Theorem and then PR bit-by-bit from there if people are interested in more? Where should I even plan to put these files?

@Scott Morrison once suggested putting social choice theory and combinatorial game theory in their own home. I have long-term hopes to formalize more results in social choice theory, game theory, and microeconomic theory if that affects how we think about this.

[Yaël Dillies]

Start by opening some PR for the preliminary lemmas. Then you can PR Arrow's theorem in several go. I don't quite know where it belongs. combinatorics.social or order.social both sound like decent places to me.

[Andrew Souther]

Also, I have been in contact with Eric Pacuit and Wesley Holliday who wrote this paper on Voting Theory in Lean. In the next few months, we plan to merge our code into one unified framework. They are real experts in social choice theory (I am not), and they have offered to help guide the conversation about design choices for a useful social choice library going forward.

[Yaël Dillies]

Then I would advise you to coordinate with them first. You do not have a huge amount of code, so PRing to mathlib should go smoothly. I see Eric Pacuit is already here, by the way!