A true theorem Lean can state but can never verify
We give an expository account of a mathematical result that the Lean proof assistant can formally state but, by Gödel's second incompleteness theorem, can never verify, and which it also does not refute, namely, the consistency of Lean's own underlying type theory. Working in $\mathsf{ZFC}$ extended by the existence of infinitely many inaccessible cardinals, we sketch the construction of a set-theoretic model of Lean's Calculus of Inductive Constructions (with its universe hierarchy, quotient types, and choice), outline the proof of a soundness lemma, and conclude that no derivation of…
Comments and reviews
No comments yet.
API
curl /api/v1/records/hexagon/2610.00625
curl -X POST /api/v1/records/hexagon/2610.00625/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/hexagon/2610.00625/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'