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

[Adrien Champion]

Adrien Champion said:

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

I'm currently working on this, but I'm struggling to get familiar enough with Fintype, Finset, Multiset, Quot... to write what I want, in particular computable definitions

[Adrien Champion]

I could use some mentoring on these things, maybe @Eric Rodriguez or @Yury G. Kudryashov ?

[Shreyas Srinivas]

There is a Finite type in mathlib

[Shreyas Srinivas]

But in general if you want to enumerate the finite set, Fintype is the best bet.

[Yury G. Kudryashov]

I'm pretty busy at my day job these days. I can answer specific questions (preferrably with some specific result you want to formalize).

[Yury G. Kudryashov]

Generally,

• if you need cardinality, then Fintype.card/Finset.card have more API than noncomputable Nat.card/Set.ncard (though improvements for Nat.card/Set.ncard are welcome);
• if you don't need [Fintype] to state the theorem, then you can assume Finite, then do cases nonempty_fintype α, if you need it for the proof.

[Adrien Champion]

I'm looking for mentoring in the general approach, I don't have a lot of experience writing complex proofs. My original proof was very "dev-oriented", for instance to show that a max exists in a (finite) quasi-preorder I would just fold over the list of elements and retrieve a max (see here)

[Adrien Champion]

But now that I'd like to write a mathlib version, I'm wondering whether it is idiomatic both for mathlib in general and w.r.t. how Fintype is supposed to be used in particular

[Adrien Champion]

To replace the previous, dev-oriented version, I currently have this

[Adrien Champion]

I'd like to get on the least-wrong track early to hopefully merge something in mathlib eventually, but as I'm very much a total noob in proof architecture it's proving difficult; not to mention I'm not super familiar with mathlib

[Eric Rodriguez]

Hi Adrien, similarly to Yury I'm pretty busy sorry to say. Your code formatting is a little un-idiomatic - we tend not to indent for namespace, for example; #style may be a good place to start there. It seems to me you wrote stuff in a very constructive way - is this your aim?

[Yury G. Kudryashov]

Note that most of Mathlib is non-constructive.

[Adrien Champion]

It seems to me you wrote stuff in a very constructive way - is this your aim?

Yes, as mentioned several times above being constructive whenever possible was a goal when I wrote the original version.

[Adrien Champion]

Yury G. Kudryashov said:

Note that most of Mathlib is non-constructive.

Yes that's why I was wondering whether my approach made sense for merging in mathlib. Sadly it doesn't, and I don't have the skills nor the interest to do a non-constructive version. Would be a different story if I had infinite time/money as I wouldn't mind acquiring these skills, but I don't have infinite time/money so... :confused:

[Eric Wieser]

I think your Finite is mathlib's docs#FinEnum?

[Eric Wieser]

Also, I think things would be easier for you if you dropped ProtoOrder and use docs#Preorder instea

[Adrien Champion]

Eric Wieser said:

I think your Finite is mathlib's FinEnum?

First time hearing about it, sounds right, thanks!

[Eric Wieser]

Though unless your computation is really order-dependent, you should be able to use Fintype instead

[Eric Wieser]

(but if you want to remain constructive, you should indeed avoid Mathlib's Finite)

[Adrien Champion]

That's what the new version draft does

[Bulhwi Cha]

@Adrien Champion Would you like to see a constructive version of Mathlib?

[Adrien Champion]

I don't think so no, I'm not sure it makes sense for most things in mathlib, does it?

[Bulhwi Cha]

I think Lean's library of constructive mathematics should be separated from Mathlib.

[Shreyas Srinivas]

In social choice theory, being constructive in some places is helpful since quite a few proofs are just algorithms

[Shreyas Srinivas]

But generally it is nice to pick and choose, since there are indeed existential results. For example the proof of existence EF1 indivisible allocations is constructive, while the proof of existence of envy free connected continuous cake division is existential

[Bulhwi Cha]

If you keep the constructive version of your work, perhaps we can include it in ConsMath (Lean's constructive mathematics library) later.