Voting theory in the Lean theorem prover

DOI10.1007/978-3-030-88708-7_9OpenAlexW3200122939MaRDI QIDQ2148823

Eric Pacuit, Chase Norman, Wesley H. Holliday

Publication date: 24 June 2022

Full work available at URL: https://arxiv.org/abs/2110.08453

zbMATH Keywords

voting theoryinteractive theorem provingLean theorem proverlogic and social choice theory

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Uses Software

• Isabelle/HOL
• Mizar
• Lean
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• First-order logic formalisation of impossibility theorems in preference aggregation
• Discovering theorems in game theory: two-person games with unique pure Nash equilibrium payoffs
• Independence of clones as a criterion for voting rules
• A new monotonic, clone-independent, reversal symmetric, and condorcet-consistent single-winner election method
• Reasoning about social choice functions
• On the role of language in social choice theory
• Twitching weak dictators
• The calculus of constructions
• Repairing proofs of Arrow's general impossibility theorem and enlarging the scope of the theorem
• Weak independence and veto power.
• Three brief proofs of Arrow's impossibility theorem
• Arrow's decisive coalitions
• Verifying randomised social choice
• A note on Murakami's theorems and incomplete social choice without the Pareto principle
• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• The Existence of Social Welfare Functions
• The Lean Theorem Prover (System Description)
• Mathematics and Politics
• The Single Profile Analogues to Multi Profile Theorems: Mathematical Logic's Approach
• Condorcet Social Choice Functions
• Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving
• Dependence and Independence in Social Choice: Arrow’s Theorem

This page was built for publication: Voting theory in the Lean theorem prover