Anchor · for Lean statements · open source
Check what a Lean theorem actually says.
Lean checks that a proof proves its statement. Anchor checks the statement itself: whether its hypotheses can all be true together, whether each one is needed, and which definitions a reader must read. Each answer is a theorem the Lean kernel accepts.
Read the film
This problem is on one of the standard tests for AI at math. The proof is one line, and Lean, the proof checker, accepted every step. I was about to sign off. He was right to stop me. The proof is fine. The problem is impossible. It's written in whole numbers, where a quarter rounds down to zero. So its one assumption can never be true. And from something impossible, you can prove anything. Lean doesn't mind. It checks the proof, not the question. Anchor checks the question. Machines now write proofs faster than anyone can read them, and tests like this keep score. So Anchor read the whole test. Four hundred and eighty-eight problems. Two start from assumptions that can never be true: free points for any prover. One is simply false. And twenty-nine carry an assumption that does no work at all. In two thousand statements from Mathlib, three more. Anchor asks every statement two questions, and every answer is a proof that Lean checks. Can its assumptions all be true at once? It finds an example where they are. Does each one matter? It takes each away and looks for a case where the conclusion fails. It also lists what you'd have to read to know what the statement says. Its search can come up empty. But it never reports a finding it hasn't proved. So now, before I sign, I check both. The proof, and the question. Anchor is free and open source. Paste in a Lean file, and see what your theorem really says.
theorem golden_of_costly_join
(s : ℕ → ℝ) (r : ℝ) (a b : ℕ)
(hstep : ∀ n, s (n + 1) = r * s n)
(hearlier : a < 2 ∧ b < 2)
(hjoin : s 2 = s a + s b)
(hcost : 0 < J (s b / s a)) :
r = goldenRatio
A ladder of levels, each r times the one before. Level 2 is the sum of two earlier levels, and comparing those two parts costs J x = (x + 1/x)/2 − 1. If that cost is positive, r is the golden ratio.
hypotheses: [0] ∀ n, s (n + 1) = r * s n [1] a < 2 ∧ b < 2 [2] s 2 = s a + s b [3] 0 < J (s b / s a) conclusion: r = goldenRatio nonvacuous: proved (supplied) hypothesis [0] load-bearing: proved (supplied) hypothesis [1] load-bearing: proved (supplied) hypothesis [2] load-bearing: proved (supplied) hypothesis [3] load-bearing: proved (supplied) verdict: CERTIFIED surface: 1 to read, 0 pinned, 33 at the boundary
Abridged. Select a line to see what it means. The kernel checked each line as a theorem, using only propext, Classical.choice and Quot.sound.
Theorem 2 of A Costly Join Forces the Golden Ratio, Recognition Physics Institute. The paper (PDF, 4 pages) Its Lean file (Mathlib only)
Every line of the report is a model you can draw.
Anchor splits the theorem into hypotheses and a conclusion and proves the split matches the original. Then it looks for models, meaning concrete examples. One model must satisfy every hypothesis. For each hypothesis, another must satisfy all the others, fail that one, and fail the conclusion too. These five ladders are the models behind the golden-ratio report.
φⁿ. Its first join is s2 = s0 + s1, which costs J(φ) ≈ 0.118. Here r = φ.1, 2, 3 join as 3 = 1 + 2 at cost J(2) = 0.25. The ratio changes from step to step, so there is no single r.φ⁻ⁿ, s2 = s3 + s4: the join uses later levels, the ladder runs downward, and r = 1/φ.s2 = 4, sits above the red line at 1 + 2, so the join fails. With no join, any ratio can occur; here r = 2.s2 = s1 + s1. Equal parts cost J(1) = 0, so the cost premise fails and r = 2. The cost is what rules doubling out.the two parts of the first join, and the level they makenumbers on top: the ratio from one level to the next
- hypotheses, conclusion
Anchor’s reading of the statement, which is checked, not trusted. If Anchor misreads your theorem, its equivalence proof fails.
- nonvacuous
Some model satisfies every hypothesis, so the theorem is about something. The golden ladder is that model (first panel).
- [0] load-bearing
Without one ratio at every step, there is no single
rto determine (second panel). - [1] load-bearing
The parts must come from earlier levels. Otherwise the ladder runs the other way and
r = 1/φ(third panel). - [2] load-bearing
Without a join, nothing relates the levels and any ratio survives (fourth panel).
- [3] load-bearing
The cost is what selects the golden ratio. Equal parts compare at no cost, and then the ladder doubles (fifth panel).
- verdict
CERTIFIED means every line above was proved. The others are
VACUOUS(the hypotheses contradict each other),DECORATIVE [k](hypothesis k can be dropped),TRIVIAL CONCLUSION(the conclusion is true of everything), andUNCERTIFIED(the search found neither a model nor a contradiction, which says nothing about the theorem).
Anchor finds models by searching small literals. These models are sequences, which that search can’t build, so the paper supplies them as theorems under Anchor’s obligation names. A supplied proof counts like a found one: the kernel checks it against Anchor’s statement of the obligation and rejects a proof of anything else.
One definition, and two conventions to check.
J x = (x + x⁻¹) / 2 − 1, the cost of comparing two parts in ratio x. A referee reads the statement and this definition.
Standard definitions from Lean’s core library and Mathlib: numbers, arithmetic, order and the golden ratio. Two conventions are flagged, x / 0 = 0 and 0⁻¹ = 0. They matter here only when a part is zero. Then J(0) = −1, the cost premise is false, and the theorem makes no claim. The paper says so in a remark.
What the referee sees.
Pith is building this into review. When a paper comes with Lean, Pith builds it in a sealed container and gives the referee one card per result: the paper’s statement beside its Lean statement, the definitions to read, and what the kernel established. This is the card for Theorem 2.
In the paper
Let s : ℕ → ℝ, r ∈ ℝ and a, b ∈ ℕ satisfy
s(n+1) = r·s(n)for everyn,a < 2andb < 2,s(2) = s(a) + s(b),J(s(b)/s(a)) > 0.
Then r = φ.
In Lean
theorem golden_of_costly_join
(s : ℕ → ℝ) (r : ℝ) (a b : ℕ)
(hstep : ∀ n, s (n + 1) = r * s n)
(hearlier : a < 2 ∧ b < 2)
(hjoin : s 2 = s a + s b)
(hcost : 0 < J (s b / s a)) :
r = goldenRatio
J, one definitionpropext, Classical.choice, Quot.soundOn a revision, the referee rereads only the cards whose statements changed. A sign-off records a hash of the statement and its surface. Editing a proof leaves it current; editing the statement, or a definition it relies on, makes it stale.
Hypotheses that do nothing, and statements about nothing.
Add the natural-looking assumption that every level is positive, and Anchor shows it can be dropped. The cost premise already forces the two parts to be nonzero and of the same sign, because J is negative on negative numbers.
theorem golden_of_costly_join_with_positive_levels …
(hpos : ∀ n, 0 < s n) …
hypothesis [0] removable: proved (proof term: the proof never uses this hypothesis)
verdict: DECORATIVE [0]
We also ran Anchor on a stratified sample of 2,000 Mathlib theorems and on all 488 statements in miniF2F. AnchorTest/Findings.lean re-derives each finding below whenever the repository builds.
- Mathlib
Three statements need one hypothesis fewer than they state: midpoint_le_right without the instance PosSMulReflectLE k E, mul_nonneg_iff_left_nonneg_of_pos without PosMulStrictMono R, and FractionalIdeal.mul_inv_cancel_of_le_one without its second hypothesis, which only guards a junk value of the inverse.
- miniF2F, two vacuous
Natural-number division turns
1 / kinto0fork > 1, and subtraction stops at0. The hypotheses of mathd_algebra_275 and mathd_algebra_289 cannot hold, so both are provable and say nothing. - miniF2F, one false
amc12a_2020_p13 is false as written. Its equation holds for every input, so the statement claims
b = 3for everyb > 1, and its negation is a theorem.
The kernel checks every claim.
Anchor adds each finding to the Lean environment as a declaration and accepts it only if #print axioms lists nothing beyond propext, Classical.choice and Quot.sound. Neither the code that reads your theorem nor the code that searches for models is trusted. A misreading fails the equivalence proof, and a wrong model fails the kernel.
We test Anchor on forty statements with known answers: ten that should certify, ten with contradictory hypotheses, ten with a decorative hypothesis, five with no hypotheses and five whose premises depend on earlier ones. Anchor recovers every label, and two runs give byte-identical output. The suite also rejects each deliberately broken control: an empty output, mutated labels, a supplied proof of the wrong statement, and a proof that reaches Lean.ofReduceBool.
One line in your lakefile.
Anchor needs Lean v4.27.0-rc1 and the Mathlib revision pinned in its lake-manifest.json. In a project on those versions, add this line to the lakefile, write import Anchor, and run #anchor foo on any theorem. Or paste a file into the checker and Pith runs it for you.
require anchor from git "https://github.com/jonwashburn/anchor" @ "main"
| #anchor foo | Analyse foo and print the report. |
| anchor_cert foo | The same, keeping every proof Anchor found as a declaration. |
| anchor_spec foo | Extract the statement so an author can supply obligations by name. |
| #surface foo | The review surface: what a reader has to read. |
| #price foo | The classical principles the proof reaches. |
| lake exe anchor check | Recompute every sign-off in a file and fail if any is stale. |
Verdicts, added declarations and report fields are specified in docs/FORMAT.md. Anchor contains no sorry, admit or axiom.
Apache License 2.0. Copyright 2026 Jonathan Washburn / Recognition Physics Institute.
Source, issues and format specification: github.com/jonwashburn/anchor