{"id":"arxiv/2610.30433","url":"https://arxiv.org/abs/2610.30433","tags":["math.LO"],"score":0,"title":"Reflections on Trusting Lean","domain":"math.LO","source":"arxiv","authors":["Lorenzo Bresolin","Marcello Mamino"],"reviews":0,"subject":"math.LO","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-21","reactions":{}}