tchajed/coq-arrows-theorem
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
Proof of Arrow's Impossibility Theorem
21 commits 1 branch 0 tags 47 KiB
  • Rocq Prover 92.4%
  • Makefile 7.6%
Find a file
Exact
Tej Chajed 6499695775
 Note down another reference
2024-01-02 10:43:32 -06:00
.github/workflows Simplify CI workflow 2024-01-02 10:41:00 -06:00
src Set up next lemma 2024-01-02 10:19:43 -06:00
.gitignore Add a better build system 2024-01-01 21:42:14 -06:00
_CoqProject Move spec to separate file 2024-01-01 21:59:19 -06:00
coq-arrows-theorem.opam Add opam file for stdpp dependency 2024-01-02 10:36:31 -06:00
Makefile Add a better build system 2024-01-01 21:42:14 -06:00
README.md Note down another reference 2024-01-02 10:43:32 -06:00

README.md

Arrow's Impossibility Theorem

CI

Coq formalization of Arrow's Impossibility Theorem. Based on the first (informal) proof in Three Brief Proofs of Arrow's Impossibility Theorem by John Geanakoplos.

Might want to switch to A Straightforward Proof of Arrow's Theorem as a basis.