Hardy zeta: proof blueprint
Hardy's theorem is proved in Lean.
The Riemann zeta function has infinitely many zeros on the critical line. The critical line contains the complex numbers with real part 1/2. A zero is an input at which the function has value zero. This result is Hardy's classical infinitude theorem. It does not prove the Riemann hypothesis.
The theorem hardy uses the actual mathlib function riemannZeta.
Move the pointer over a Lean name to see its type.
The independent Comparator check accepts the exact statement and replays its proof in Lean's kernel.
The local check permits only the three standard logical axioms.
theorem hardy : Set.Infinite {s : ℂ | s.re = 1 / 2 ∧ riemannZeta s = 0} := ⊢ {s | s.re = 1 / 2 ∧ riemannZeta s = 0}.Infinite
All goals completed! 🐙Open the Lean repository · Examine the full theorem check
The repository is private. The checked source is also available on this site.