math.LO — Logic

A true theorem Lean can state but can never verify

Contributed by William Banks

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 $\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.