Machine-Checked Economics: When Computers Verify Proofs

Abstract. Every theorem in the CES framework is formalized in the Lean 4 proof assistant, with zero unproved claims, 99 marquee theorems verified, and only three classical axioms -- making this the first machine-checked body of economic theory.