Topic: Social Choice in mathlib
Andrew Souther (Nov 20 2021 at 18:04):
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:
basicfile, 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.
arrows_theoremfile, 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 (Nov 20 2021 at 18:10):
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.
order.social both sound like decent places to me.
Andrew Souther (Nov 20 2021 at 18:12):
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 (Nov 20 2021 at 18:20):
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!
Last updated: Aug 03 2023 at 10:10 UTC