Papers With

← All papers
First page of Reflections on Trusting Lean

Reflections on Trusting Lean

Lorenzo Bresolin, Marcello Mamino

math.LO Oct 21, 2026 · v1
formalization type-theory logic
Read PDF arXiv abstract Code
TL;DR
Studies the metatheory of Lean 4's type theory and implements one direction of the arithmetic-conservativity proof in Lean 4.
Abstract
It is known, by works of Werner and Carneiro, that the type theory of Lean (and indeed of CIC plus a version of choice) is equiconsistent with ZFC plus "there are infinitely many strongly inaccessible cardinals". We prove a finer connection between these two formal systems; namely, given any formula in the language of second order arithmetic, that formula is provable in the aforementioned extension of ZFC if and only if the same formula, when viewed as a type in Lean, is inhabited.
Problem

Lean's type theory (CIC plus choice, propositional extensionality and proof irrelevance) is known to be equiconsistent with ZFC plus infinitely many strongly inaccessible cardinals. Equiconsistency alone does not guarantee that the two systems prove the same statements.

Approach

Translations of second-order arithmetic formulas into both Lean's type theory and ZFC_∞ are defined. Werner's set model inside CIC is used for one direction. Carneiro's set-theoretic model of Lean, via its reduction to W-types, is used for the converse. The implication from the internal ZFC_n model to the Lean statement was implemented in Lean 4.

Results

A second-order arithmetic sentence is provable in ZFC_∞ if and only if its translation, viewed as a Lean type, is inhabited. So Lean proofs of arithmetic statements, such as the twin prime conjecture, are as trustworthy as ZFC_∞ proofs.