Here are some useful fundamentals that I found helpful assuring myself that LEAN works:
The Foundational Systems Underneath
Lean is based on dependent type theory, an alternative foundation as ZFC. (Lean is strictly stronger than ZFC, roughly ZFC + ω inaccessibles.) (“Dependent” means types can depend on values). But note that the continuum hypothesis is independent of Lean too.
Proposition as Types
Reference: Philip Wadler Proposition as Types (2014). Section 6 and 7.
Claim: there is an exact correspondence between a logic and a typed programming language. A proposition is a type. A proof is a term, or a program. Proof simplification evaluate whether a program output a term that belongs to the type that the proposition corresponds to.
| Logic | Computation | Lean |
|---|---|---|
| proposition | type | P : Prop |
| proof | term (program) | h : P |
| proof simplification | evaluation | (fun x => N) M ⟶ N[M/x] |
NOTE: in LEAN checking somtimes use axiom of choice, and the computation might get stuck. Also, LEAN does require all definitions to terminate: def bad : False := bad is not allowed.
Hilbert’s 10th and autoformalization
Roughly speaking, no autoformalization is 100% trustworthy. Formally, no algorithm can, for every input, either output a faithful translation of the proof to LEAN or correctly reject the proof.
The argument in Bastounis et al. (2026 Arxiv):
- Consider a definition like “n_e = the least n such that ∀x, p_e(n, x) ≠ 0.” where {p_e}_{e in N} are polynomials in k + 1 variables with interger coefficients. A faithful translator must tell whether n_e exists, and refuse to translate if it doesn’t.
- Hilbert’s 10th turns “machine e halts” into “polynomial p_e has a root.”
- Hence “does n_e exist?” is as hard as “does some machine fail to halt,”
Thus, when a translator encounters ambiguity or hidden presuppositions in natural language proof, they can expose them as explicit hypotheses instead of deciding them. Thus, for an AI written LEAN proof, LEAN does verifies that the proof matches the statement as written. But errors can still hide in junk values (sInf ∅ = 0, x / 0 = 0, 5 - 7 = 0 in ℕ) and in mistranslated definitions.