An attempt to formalize apportionment theory, a part of social choice theory, in Lean. Documentation is available.
| statement | progress |
|---|---|
| Balinski–Young impossibility theorem | ✅ done |
| divisor methods are in fact methods (ABCDE properties) | 🏗️ in progress |
| largest remainder methods are in fact methods (ABCDE properties) | 🏗️ in progress |
| coherence theorem(s) |