HackerPapers

arXiv:2610.30433math.LO

Reflections on Trusting Lean

Lorenzo Bresolin, Marcello Mamino

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

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.

arXiv comments
This work has been presented at ICMS 2026 on 23 July 2026
Journal reference
DOI
Subjects
math.LOLogic

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Oct 2026 to Oct 2026. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.