Not summarized, not reviewed, not "looks right" — compiled. Here is exactly what that buys you.
Every proof is checked, step by step, against a pinned library of 202,827 formalized results. If one step fails, nothing passes.
Each result shows the exact axioms it rests on — never collapsed into a tick.
axioms: [propext, Classical.choice, Quot.sound]
Incomplete proofs, compiler-trust shortcuts, and theorems with contradictory hypotheses are rejected with the reason. What we refuse is part of the guarantee.
Two proofs of the same theorem are one fact with two routes — search never shows you the same result twice, and every record names who built on it.
| verdict | what it tells you |
|---|---|
| verified | Proof compiled; axioms within the standard three.1 |
| conditional | Proved assuming named open statements — the kernel tracks the assumption, and the result upgrades automatically the day it's proved. |
| statement_only | A conjecture: well-formed and citable, with nothing claimed about its truth. |
| rejected / incomplete / vacuous | Refused, with the reason shown. |
sorry into a proof —
watch it refuse, right on the homepage.Fine print, stated plainly. Verification is precise about what it covers:
1. Machine-checked means the proof proves the stated theorem. Whether a formal statement captures its author's intent2, whether hypotheses are satisfiable beyond our automatic probes and witnesses3, and whether a result is novel or significant, remain human judgements — as everywhere in mathematics.
2. Formalisation faithfulness is not machine-decidable; we store the source statement alongside so you can always compare.
3. We reject provably-contradictory hypotheses automatically and record a witnessed flag when a concrete instance has been exhibited; null means not yet checked, and we say so rather than guessing.
4. Proofs are checked against a pinned mathlib (Lean v4.27.0); moving the pin is a deliberate, recorded migration.
LemmaHub · lemmahub.org · Renaud Rivier & Simon Janin