cert-machine · report · generated from the records
Does an AI’s Lean proof prove the right statement? One command to check
A Lean proof can be correct and still prove the wrong thing. Lean’s kernels check the proof; this tool checks the statement, with exact tests instead of a reader’s opinion. Two AI-written refutations of Erdős problems, waiting on Google DeepMind’s list of open problems, went through it.
Lean’s kernels answer the first question. The second is the one this tool adds: the same statement, wrong ones refused, and the statement compared with the problem’s own words on small cases.Records: certs/lean-intake-erdos-488.json · sha256 3d55fa1fe80a; certs/lean-intake-erdos-786i.json · sha256 98066cbd66c4
claims checked
2
Erdős #488 and #786(i)
planted wrong statements refused
16 of 16
and 10 of 10 rewordings accepted
planted defects caught
7 of 7
a false step, a sorry, an axiom, native_decide
a fresh claim, rules to record
51 min
on a laptop
The mathematics is the claimants’ (Declan Gessel’s, with OpenAI’s GPT-6 Astra, for both refutations); the statements are Google DeepMind’s. This page checks their proofs against those statements. The tool is mine, built with Claude (Anthropic).
read this first
What it does not decide
Whether the formal statement is the problem. That stays a reading; the small cases are evidence, not proof.
“The same” means the same after unfolding definitions. Statements equivalent only by an argument are refused (all 3 planted ones were).
Small cases compare true and false. A change that never flips an answer there is invisible to them.
Some statements have no small cases. #786(i) is about densities of infinite sets: refused there, as planned.
Four of Lean 4.35’s bundled checkers were not run. Both claims are on Lean 4.33.1; leanchecker-paranoid, lean4lean, con-leche, con-ron come later.
does the check work?
Every planted test came out as it should
Each run tests the check itself. Wrong versions of the statement are planted (a dropped hypothesis, a changed constant, a shifted interval) and must be refused; rewordings of the same statement must be accepted; broken copies of the proof must be caught. One square per test; hover for what it was.
The planted tests of both runs. The three filled squares in the third row are the stated limit: statements that are logically the same but differ by more than unfolding a definition are refused.Records: certs/lean-intake-erdos-488.json · sha256 3d55fa1fe80a; certs/lean-intake-erdos-786i.json · sha256 98066cbd66c4The build refuses this figure if a planted statement or defect is not as expected.
Erdős #488
DeepMind’s statement against Erdős’s sentence
Erdős asked whether, for a finite set A and B the numbers with a divisor in A, |B ∩ [1,m]|/m < 2|B ∩ [1,n]|/n always holds for m > n ≥ max(A). Gessel’s proof refutes DeepMind’s Lean version of it; this run reached the same verdicts as a separate hand-built check of 6 November.
Then the new check: Lean evaluated DeepMind’s statement part by part on 3,024 small cases (the kernel confirmed every value), and a program written from Erdős’s sentence alone evaluated the same cases.
Every part agrees wherever Erdős’s sentence makes sense. The 20 cases where the whole statements differ all have A = {0}: B is empty there, the sentence reads 0 < 0 and is false as written. DeepMind’s statement adds the hypothesis 0 ∉ A for exactly this (their pull request #256); the check found the reason without being told.Records: certs/lean-intake-erdos-488.json · sha256 3d55fa1fe80a; instruments/intake/erdos-488.js · sha256 a2dc8058927bThe build refuses this figure if the cases stop adding up, or a disagreement is not one with A = {0}.
Erdős #786(i)
A claim the tool had not seen
Part (i) asks whether some set of density above 1 − ε has all its equal products of equal length. Gessel’s refutation (pull request #5299, open since 6 September) states its own versions of the two definitions it needs. The kernel accepts it against DeepMind’s declaration as it stands today, so the definitions match.
It also turned up one thing for the pull request: DeepMind reworded this statement on 14 October, so the change no longer applies and GitHub reports a conflict. The proof still refutes the current statement.
From the spec committed to the record, on a laptop. The first run found a defect in the tool (its test files missed one line of DeepMind’s file); it was fixed and the planted statements run again, with no statement or expectation changed.Records: certs/lean-intake-erdos-786i.json · sha256 98066cbd66c4; corpus/lean-intake/erdos-786i/runs/2026-11-09/_status.txt · sha256 16a5b9f23555The build refuses this figure if the clock falls out of order.
what I got wrong
Four corrections, made in the open
#488: a “wrong” statement was the same. Counting from 0 changes nothing, since 0 is never counted; the kernel saw it. My label was wrong (14 of 15 as first written).
#488: the small cases found more than I expected. The 20 cases above, all explained.
#488: one planted statement was invisible to the small cases. Counting from 2 changes counts, never answers: the limit, measured.
#786(i): a defect in the tool. Fixed and re-run; then 12 of 12 came out as written.
Each spec was committed before its run, and each correction is a dated amendment beside the first outcome.