Push the boundary of knowledge

What the Lean API is, and how you use it

Every question here has exactly one canonical Lean statement — its API. It is what makes what is being asked a question with one answer, and is this proof correct a question a machine can settle.

1. 1

   Someone asks, in English

   No Lean, and no formalization. You describe the question, say why you think it is open, and attach the papers that make the case.

2. 2

   A maintainer writes the Lean API

   One canonical def goal : Prop, with every term in it bound to a definition you can unfold. A named researcher signs off that the Lean means what the mathematics means — the one judgement no machine can make, and nothing goes live without it.

   The Riemann hypothesis

   import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
   import Mathlib.NumberTheory.LSeries.RiemannZeta
   
   namespace Conjectura.AN002
   
   /-- Every non-trivial zero of the Riemann zeta function has real part `1/2`. The
   trivial zeros are the negative even integers, excluded here by restricting to the
   strip where the real part lies strictly between zero and one. -/
   def goal : Prop :=
     ∀ s : ℂ, riemannZeta s = 0 → 0 < s.re → s.re < 1 → s.re = 1 / 2
   
   end Conjectura.AN002

3. 3

   You download that exact file

   Not a transcription — the same bytes the checker will use, with every definition it depends on brought along. So a proof you develop against it is a proof against the real statement.

4. 4

   The kernel checks your proof against it

   It has to typecheck as a proof of goal itself, not of something that resembles it. Axioms are audited, so sorry and native_decide cannot slip past — and anyone can re-run the same check and get the same verdict.

5. 5

   The answer comes back in English

   A verified proof is written back into prose so it can be read. A rejected one is told where the argument breaks, rather than handed a wall of compiler output.