PreprintarXiv licencearXiv
Reflections on Trusting Lean
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.
Related
- Lie (super)algebras generated by reflections in finite reflection groups of exceptional type
- Möbius Maps, Reflections and Lipschitz Constants
- Cyclic reflections and the flip equation for the graded Grothendieck-Teichmüller group
- Symmetric two-level preconditioning for the method of reflections
- Dynamics of Hyperbolic Schwarz Reflections
BibTeX
@misc{bresolin2026reflections,
title = {{Reflections on Trusting Lean}},
author = {Lorenzo Bresolin and Marcello Mamino},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.30433},
eprint = {2610.30433},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.30433},
}
RIS
TY - UNPB
TI - Reflections on Trusting Lean
AU - Lorenzo Bresolin
AU - Marcello Mamino
PY - 2026
DA - 2026/10/21
PB - arXiv
DO - 10.48550/arxiv.2610.30433
UR - https://arxiv.org/abs/2610.30433
AB - 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.
ER -