The landscape
Grouped by what kind of record each keeps. These descriptions come from the file that also renders them beside a citation, so the two cannot disagree.
Machine-checked elsewhere
Incubated by the Lean FRO and ICARM, with a scientific advisory board of nine mathematicians.
Snapshots of public Lean repositories, mathematics only.
CertifiesA Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review.
A platform publishing authored formalizations, in read-only beta.
Lean formalizations and the proof routes behind them, mathematics only.
CertifiesThat a recorded Lean build passed with no unfinished proof steps, under its own evidence contract, which a record can satisfy for checking while still failing for acceptance.
The open problem
A collaboration between Caltech mathematics faculty, graduate students and undergraduates.
66,736 open problems in research mathematics.
CertifiesNothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.
Also recorded at
Community-curated, maintained by Rasmus Lindahl.
Mathematics problems first closed with AI in the loop.
CertifiesNothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
One result, four different facts
Sendov's conjecture sits in all four. ProofAtlas hosts Lech Mazur's formalization, marked Lean checked but not accepted: its retained audit is a summary, not the full build transcript. Palomar registers Terence Tao's separate formalization and archives its whole dependency tree. MathDB tracks the conjecture. vibemathed lists the result.
All four are true at once. Priority for the first machine-checked proof is Mazur's; the reproducible archived artifact is Tao's. Our entry for Sendov is the only place both appear together.
The Jacobian conjecture shows it sharper. MathDB records it partially solved, the claim not independently verified. We grade the counterexample formally verified. Both are right: they track the conjecture's standing in the literature, which stays open until the literature catches up, and we grade whether the counterexample checks out, which it does in seconds by symbolic recomputation.
What none of them do
We grade how much the AI did. Every entry carries an autonomy grade on a six-point scale, from a result the model produced with no input beyond the problem statement down to one it retrieved from the literature. Arguable cases take the weaker grade.
We keep the failures. Refuted, disputed and already-known results stay on the record. One entry covers ten Erdős problems an AI was reported to have solved and had in fact located existing solutions to. A project that registers only successes has nowhere to put that.
We also carry the case against: every source is labelled with what it is, and challenge is one of the labels. Where an entry has no counterargument, the review queue says so rather than letting silence read as consensus.
Every project above is mathematics only. Half this registry is not.
Corrections welcome
If you maintain one of these and this page has it wrong, we would rather hear it. Send a correction or email us. A fix lands here, on the methodology page and beside every citation at once.