Arrow's Impossibility Theorem

Stream: general

[Andrew Souther]

This summer, @Benjamin Davidson and I formalized Arrow's Impossibility Theorem in Lean! We have our Lean project on my GitHub. This theorem has been formalized before in Mizar and HOL, but it was a fun project.

Eventually, I'd like to formalize some more Social Choice Theory or Microeconomic Theory in Lean.

[Scott Morrison]

Are we going to have a social_choice/ folder in mathlib soon?

[Scott Morrison]

In the meantime, you may want to set up the github action that keeps bumping mathlib (so that your repository doesn't bitrot).

[Scott Morrison]

You may also like to add your project to https://leanprover-community.github.io/lean_projects.html

[Andrew Souther]

I would be very happy trying to prepare a social_choice folder... I wasn't sure if people would be interested in this kind of work on mathlib.

[Andrew Souther]

At the very least, I would like to add it as a project and set up that action.

[Scott Morrison]

I've heard talks about Arrow's theorem in maths departments, and therefore it's maths, and therefore it's welcome in mathlib?

[Scott Morrison]

I doubt we should have a top-level social_choice/ folder quite yet. I'm not really sure where to put it. We have combinatorial game theory under set_theory. Perhaps there, or perhaps both of games and social choice should find a new home together.