What this is
AI-generated text
A for-loop over the Erdős problems
erdosproblems.com catalogs 1179 problems posed by Paul Erdős, open and solved alike. When this project began, Google DeepMind's formal-conjectures repository had Lean statements for 374 of them. This project wrote the other 805, completing Milestone 1: all open Erdős problems formalized. It then wrote its own versions of DeepMind's 374 as well, so this repository has a first-pass Lean file for all 1179.
The idea came from formalizing one by hand. After contributing problem 13 to DeepMind's repository, it was clear that the remaining 805 weren't a research problem so much as a loop: run the same prompt on every problem, and pay for the tokens.
This work contains no proofs. Every theorem ends in sorry, Lean's placeholder for a missing proof. What the project produces is the statement: the problem written precisely enough in Lean that a proof of it, if anyone finds one, can be checked by machine. Next to proving, stating sounds like the easy half. It isn't, and checking the statements is what most of this page is about.
Why stating a problem is hard
A formal statement can compile perfectly and still be the wrong claim. It can be trivially true, so proving it establishes nothing, or trivially false, so no proof exists. It can assert the opposite of what the problem claims, or state as true a conjecture that has since been disproved. Lean checks that a statement is well-formed, not that it says what the problem says. Checking that it is faithful is the second pass's job.
First pass
AI-generated text
Formalization
Claude took each of the 805 new problems through four stages:
The Style, Review and Fix stages worked on copies formatted for DeepMind's repository, now archived in deepmind/. The second pass starts from the Formalize stage's output in conjectures/.
The setup was simple: a tmux session on a small cloud server (2 vCPUs, 4 GB of RAM), left running for days:
$ cat todo-conjectures.txt | xargs -I % claude --dangerously-skip-permissions \
"Read FORMALIZE_CONJECTURE.md. Apply to problem %.
Write output to conjectures/%.lean. Ensure `lake build` passes."
The bottleneck was the Claude subscription's usage limits, not compute. The weekly token allowance ran out twice, and the run waited for it to reset each time. Running problems in parallel didn't help: it hit the per-session limit sooner without finishing any faster, so the loop went back to one problem at a time.
Second pass
AI-generated text
Adversarial review
The first-pass files are drafts. The second pass gives each problem to a stronger model, Claude Fable 5, with a different brief: assume the formalization is wrong, and find out how.
How a review works
Each problem gets its own agent and its own commit. The agent works from a saved copy of the original erdosproblems.com page rather than from memory, works through the mathematics for itself, rechecks the first-pass review claim by claim, and writes up to two files: a corrected conjectures-v2/N.lean and a review note, fable-review/N.md. It never edits the first-pass file, so every correction can be read as a clean before-and-after pair.
What gets checked
Part A · Semantic fidelity
Does the Lean say what the source page says? This covers Lean-specific traps, errors in helper definitions, yes/no questions answered the wrong way round, and the problem's current status, which may have changed since the page was saved.
Part B · Scholarship
Every cited reference is defined, with details taken from a real source, never invented. Variants of the problem mentioned on the source page are included.
Part C · Craftsmanship
Readability, docstrings that match the code beneath them, reuse of Mathlib rather than reinvention.
Part D · Mechanical checks
Text searches for known problem patterns: sorry outside a proof, fragile tactics, misplaced binders, missing docstrings.
Part E · Prior-review audit
Every claim the first-pass reviewer made, rechecked from scratch.
Two standing rules
Never fabricate a citation. Where a journal, volume, or page number could not be found in a real source, the entry says it is missing instead of guessing. A plausible-looking fake reference is worse than an admitted gap, because it survives review.
Work from the source, not from memory. A model's memory of a famous problem is exactly where subtle misstatements come from. In the most recent batch (problems 1–90), every review worked from a saved copy of the problem page and checked the problem's status against an independent source such as the teorth/erdosproblems database, because problems get solved after a page is saved.
Findings
AI-generated text
What the reviews found
270 problems have been through the second pass. Not one came back clean. Every file needed at least documentation fixes, and about a third (93 of 270) had an error serious enough to change what the statement means.
Three kinds of defect
The interesting errors are the ones a compiler can't see. They fall into three groups.
Polarity. The Lean asserts the direction the source says is false: it states a disproved conjecture as true, or leaves out the answer(False) marker that records a yes/no question's answer as no. The statement looks flawless and says something false, which makes this the most dangerous kind.
Vacuity and degeneracy. The statement is provable, or refutable, for reasons that have nothing to do with the mathematics. The same causes keep coming up:
- Mathlib's placeholder values at inputs where a function is undefined, such as
Real.log 0 = 0, sInf ∅ = 0, rpow 0 0 = 1 and φ(0) = 0;
- an optional parameter left unconstrained, so a definition can be used outside the range it was meant for;
- a constant placed after a variable it should not depend on, so it can absorb the very growth the problem is about;
- a bound that is simply false for small
n, because log log n is negative there.
Bibliography. References cited but never defined, references with no publication details, and results attributed to the wrong paper.
Case files
AI-generated text
Three catches and a miss
Counts don't show what these errors look like. Here are three that the second pass caught, and one where the second pass itself was wrong:
90A conjecture disproved after it was formalized
The unit distance conjecture, which carries a $500 Erdős prize, was disproved in May 2026, following a construction found by an AI model. The saved copy of the problem page predates the disproof and still lists the problem as open, and the first-pass file states the conjecture as true.
Catching it meant distrusting the saved page and checking the problem's status elsewhere. The more instructive part came next. Simply negating the statement would have produced a "disproof" that any two points satisfy, because for two points the bound is false anyway (log log 2 is negative). The corrected file requires at least three points, so the negated statement says what the disproof actually says.
56An off-by-one that counting couldn't catch
A helper definition was meant to build one set and instead built a copy shifted down by one. The shifted set has the same size as the intended one but different members, so the counts checked out and the code looked right on a read-through. Listing the elements for small cases is what exposed it.
That technique — stop reading the definition, run it on n = 3, 4, 5, and look at what comes out — became standard for the rest of that batch, where eight more reviews used it to check their definitions.
55A constant on the wrong side of a quantifier
The known answer is that the sparsest sets with the property in question have about r·(log N)² elements up to N, where r is the number of colours, with constants that do not depend on r. The formalization said "for every r there is a constant" instead of "there is a constant that works for every r". That lets the constant depend on r and swallow the factor of r, the very part of the answer that matters. The statement still type-checks and is still true; it just no longer says anything about how the bound depends on r.
Quantifier order is an easy place for a formalization to go quietly wrong: both orders compile, and both read naturally in English.
86When the reviewer was wrong
The review of problem 86 concluded that writing loopless := ⟨fun …⟩ in a graph definition fails to compile, citing old build logs as evidence, and applied the same "fix" to three other files. It had it backwards. Current Mathlib defines that field as a structure, so the ⟨…⟩ constructor is required. The logs predated that change and described a version of Mathlib that no longer existed.
The next build failed on all four files, and a follow-up commit reverted them. The lesson is worth keeping: a build log shows how code behaved against the library as it was then, not as it is now, and applying one stale conclusion across many files is how a single mistake reached four of them.
Auditing the auditor
AI-generated text
The first-pass reviews were themselves unreliable
Part E of each second-pass review rechecks every claim the first-pass reviewer made. It turned up four recurring failures, which together show what automated review looks like when it goes wrong:
- Fabricated verification. Citations certified as "matching the source" when the source says no such thing: a journal and volume given for what is only an arXiv preprint, or a prize described as awarded when the page says only that the problem was proved.
- Right conclusion, wrong reasoning. A restriction (
ε < 1) correctly kept, but justified by an argument that fails whenever the exponent is even. The verdict was right; the reasoning behind it wasn't.
- Unsound "critical fixes." A proposed correction that would have made a correct statement wrong.
- Fixes that never landed. Errors correctly identified, but fixed only in the DeepMind-styled copy, never in the file under review.
The lesson goes beyond this project: confident review prose is not evidence that the checking actually happened. What makes the second pass checkable is that each of its claims points to a source a reader can open.
Benchmark
AI-generated text
Does model strength show up in the numbers?
Problems 1101–1179 were reviewed twice, independently: once by Claude Fable 5, and once by the smaller, cheaper Claude Haiku 4.5, which never saw the first review. Their verdicts came out very differently:
Haiku asked for more revisions, but most were disagreements over style. Its most common request was to rewrite a statement into the answer(…) form, which the Fable run had accepted as fine for these files; a few of those rewrites relied on a makeshift local definition of answer, or on an import from DeepMind's repository that doesn't exist in this one. Haiku also recovered the original problem page for fewer than half the problems, and accepted fabricated references in at least four. The real mathematical errors it did catch were mostly ones Fable caught too.
The takeaway isn't that cheap models don't work; it's that the two fail in different ways. That suggests splitting the work: let a cheaper model handle routine documentation, and save the stronger model for polarity, vacuity and quantifier order — the errors that take real mathematics to find.
Verification
AI-generated text
It builds
All 202 corrected files compile in this repository with lake build ErdosV2, and the only warnings are the expected declaration uses 'sorry'. That is all a successful build shows: the statements are valid Lean, and none of them claims to be proved.
The first full build after the latest batch failed on 7 of the 202 files. Four were the loopless reversal described under problem 86. The other three were ordinary Mathlib drift: a module that had become a deprecated stub, imports for definitions that had moved, and a binder whose inferred type had changed. Breakage like this is routine when building against a fast-moving library, and unlike the other errors on this page, the compiler catches it.
What is not verified
Reviewers work without a compiler; their fixes are compiled afterward, on a separate machine. References that couldn't be found are marked as deferred rather than guessed. And no human signs off on any of this, unlike DeepMind's repository, where every contribution is reviewed by a person. The second pass is the quality check.
Repository
AI-generated text
Where things live
Those headers record the verdict, the confidence, whether the source was recovered, and the defect classes, so the reviews can be searched without reading every note. The explorer is built from the same data: filter all 1179 problems by verdict, status, defect class or subject, and open any one to see its statements, review findings and sources. Regenerate its data with make site and preview it locally with make serve.
What's next
AI-generated text
A benchmark that ages well
909 problems haven't had a second pass yet. The plan is to finish them, then rerun all 1179 each time a new model ships.
The reruns are the point. Faithful formalization is an unusually clean thing to measure: the problems are fixed and public, and the only question is whether a model can restate each one in Lean without changing what it means. There is no score to game — a statement is faithful or it isn't, and a reader with the problem page can check. As models improve, the number of errors found per batch should fall, and the kinds that persist longest will be the ones worth studying.
Cost, for anyone considering the same: a second-pass review used roughly 106k–144k tokens in a sample of four recent reviews, so a 100-problem batch comes to about 12M. The subscription's weekly usage limit has been the bottleneck at every stage of this project — not compute, not the model, not the mathematics.