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!

[Adrien Champion]

@Andrew Souther I have a proof of arrow's theorem from Sen's book as well (so, the first three chapters) in Lean 4 where I made everything I could computable. What's the status on your work?

[Adrien Champion]

As far as I can tell it's not in mathlib 4 is it?

[Andrew Souther]

I haven't worked on this project much since I was a student in 2021. You're right, it never made it into mathlib. It's just sitting in an old GitHub repo. Congrats on your proof!

[Adrien Champion]

I see thanks! I'm working towards publishing my version but I want to clean it up first, I'll update this thread once I have

[Adrien Champion]

@Bolton Bailey don't be sad there's a brand new proof in Lean 4 :grinning:

[Yury G. Kudryashov]

Are you going to PR it?

[Adrien Champion]

Well once I improve the presentation and documentation I'd rather get feedback first. This is my first time working a proof that big, so I'm not sure it'll be up to mathlib's standards

[Adrien Champion]

I'm actually very confident it won't, starting with the syntax as I did not try to follow mathlib's conventions mostly because I don't know them

[Anatole Dedecker]

Actually the best way to get your code to mathlib standards is probably to open a pull request. Of course it’s better if you can start the job on your own, but you’ll probably get a lot more feedback by opening PRs than by sending some code on Zulip

[Adrien Champion]

It just hit me that, since I'm doing the whole book (well, just the first three chapters currently), I'm using mostly custom typeclasses. For preorder/quasi-order/order for instance (though they imply mathlib's). So instead of cleaning everything I did I should probably just rewrite Arrow without custom classes

[Adrien Champion]

In particular I have a custom notion of Finite-ness, as I struggled to get a computable one from Mathlib. The main issue here is that it's my first time using Mathlib at all, in everything else I did I depended only on core and sometimes std4

[Adrien Champion]

What I'm saying is that I realize now we will probably never merge anything based on what I have right now, but I can try to write a version that's more Mathlib-friendly. The issue being time/energy/actual job :confused:

[Adrien Champion]

My repository is public now. It's far from where I wanted it to be before sharing it, but hopefully it will make the conversation easier

• https://github.com/AdrienChampion/collChoSoWel

[Eric Rodriguez]

For finite, was Fintype (maybe with decidable_eq and such) not good enough for you?

[Adrien Champion]

Well the thing is, I needed a notion of finiteness early on and at that point I was still avoiding to depend on Mathlib...

[Adrien Champion]

In any case, I'll try my best to write a Mathlib-friendly version as soon as I find enough time, most likely using Fintype since my Finite class is kind of based on it