HEXAGONbeta

A true theorem Lean can state but can never verify

A mix of human-written and AI-generated textHuman understanding: all partsmath.LO — Logiccs.LO — Logic in Computer Science

Contributed by William Banks ↗

Version 1 / Oct 29, 2026 / CC BY 4.0

Abstract

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 ZFC\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 False\mathtt{False} exists. The argument is the model-theoretic consistency proof carried out in full by Carneiro, building on Werner's set-theoretic interpretation of the same calculus; all substantive results are due to these authors, and this paper claims no new mathematics. We explain why this theorem lies outside Lean's own reach, note that Gödel's second incompleteness theorem has itself been verified by Lean's kernel for first-order arithmetic, and discuss why every consistency proof ultimately rests on trust rather than proof.

Provenance statement

This is an expository paper; the mathematical results are due to Carneiro and Werner, as cited in the text, and the paper claims no new mathematics. The large language model Claude (Anthropic) was used extensively in its preparation: it produced initial drafts of much of the text, including the exposition of the proofs, and assisted with literature searches, proof checking, and brainstorming. The author directed and revised the entire manuscript, verified every mathematical claim and every reference against the cited sources, and takes full and sole responsibility for the final content. No proof assistant was used in preparing the paper; Lean is its subject, not a tool employed in it.

Tools used

Anthropic
Claude FableVersion 5.0

References

  1. M. Carneiro, The type theory of Lean. Master's thesis, Carnegie Mellon University, 2019.
  2. M. Carneiro, Lean4Lean: verifying a typechecker for Lean, in Lean. In: 31st International Conference on Types for Proofs and Programs (TYPES 2025) , Leibniz Int. Proc. Inform., vol. 384, Schloss Dagstuhl, Dagstuhl, 2026, 2:1--2:23.
  3. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language. In: Automated Deduction -- CADE 28 , Lecture Notes in Comput. Sci., vol. 12699, Springer, Cham, 2021, 625--635.
  4. The Formalized Formal Logic project, Foundation: formalization of mathematical logic in Lean 4. https://github.com/FormalizedFormalLogic/Foundation.link
  5. G. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie. Math. Ann. 112 (1936), 493--565. English translation: The consistency of elementary number theory, in M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen . Stud. Logic Found. Math., vol. 55, North-Holland, Amsterdam, 1969, 132--213.
  6. K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatsh. Math. Phys. 38 (1931), 173--198.
  7. B. Werner, Sets in types, types in sets. In: Theoretical Aspects of Computer Software (TACS '97) , Lecture Notes in Comput. Sci., vol. 1281, Springer, Berlin, 1997.

Version history

  1. v1Submitted by William BanksRevised after moderator-requested changesCurrentOct 29, 2026