What does Lean 4 actually check in a number theory proof?

People hear "machine-verified proof of the Riemann Hypothesis" and imagine the computer checking every \(\varepsilon\)-\(\delta\) argument from Rudin. That's not what happens, and the gap between expectation and reality matters.

What the machine checks

Lean 4 verifies a specific, well-defined set of properties:

1. Type correctness — every mathematical object has a declared type. If you claim \(f : \mathbb{R} \to \mathbb{R}\) is continuous, the type system enforces that \(f\) is actually a function between those types.
1. Proof chain integrity — if Theorem B says "by Theorem A and Lemma C," the kernel checks that A and C actually imply B. No hand-waving.
1. No sorry — the keyword sorry marks an unproved gap. Zero sorry means the chain is complete from axioms to conclusion.
1. Axiom inventory — every assumption is explicit. Our RH formalization has exactly 8 axioms, and they're listed.

What the machine does NOT check

1. Whether axioms are true — if I axiomatize "all primes are odd" and prove consequences, Lean happily verifies the proofs. The axiom is false (2 exists), but the proofs are valid given the axiom.
1. Faithfulness — whether my_zeta_function in Lean actually corresponds to the Riemann \(\zeta\). This is a human judgment. Mathlib's riemannZeta is well-audited, but definitions you build yourself need scrutiny.
1. Significance — Lean doesn't know if your theorem is interesting or trivial. It checks validity, not importance.

The practical consequence

When I say "the combinatorial core of the SGT is Lean-verified with 0 axioms," I mean: if you trust Lean's logic and Mathlib's definitions, the SGT is an unconditional theorem. There is nothing left to argue about.

When I say "the full RH proof has 8 axioms," I mean: the proof is valid conditional on those 8 statements. Each axiom is a precise mathematical claim that can be independently evaluated. The proof reduces RH to those 8 claims.

Why this matters for independent researchers

If you're not at a top university, your proofs face extra skepticism. A Lean-verified proof changes the conversation: instead of "I don't believe your argument in Step 7," the discussion becomes "do I accept Axiom 3?" That's a much more productive conversation.

The machine doesn't replace peer review. It replaces the most tedious, error-prone part of it.