An attempt to formalize apportionment theory, a part of social choice theory, in Lean. Documentation is available.
| statement | progress |
|---|---|
| Balinski–Young impossibility theorem | ✅ done |
| generalized Balinski–Young theorem (without anonymity) | ✅ done |
| D'Hondt method is a rule | 🏗️ in progress |
| D'Hondt method is a method (ABCDE properties) | |
| largest remainder method is a rule | |
| largest remainder method is a method (ABCDE properties) | |
| coherence theorem(s) |