| area | Registered | Checks rerun | Reading guide written | Read independently | Claim rule met |
|---|---|---|---|---|---|
| Analysis: polynomial interpolation | Erdős #671 | · | · | · | · |
| Analysis: polynomials | Erdős #1133 | · | · | · | · |
| Graph theory: Ramsey theory | Erdős #550 | · | · | · | · |
| Number theory: arithmetic functions | Erdős #1061 | · | · | · | · |
| Number theory: binomial coefficients | Erdős #731 | · | · | · | · |
| Number theory: extremal problems | Erdős #856 | · | · | · | · |
| Number theory: gaps between primes | · | Prime gaps ≤ 240 (Zhang) | Prime gaps ≤ 186 (OpenAI) | · | · |
| Number theory: multiplicative structure | · | · | Erdős #768 | · | · |
| Number theory: unit fractions | · | · | Erdős #306 | · | · |
| Set theory and hypergraphs: chromatic number | Erdős #1177Erdős #593 | · | · | · | · |
Each claim has its own repo. Status is defined in the main protocol.
| claim | stage · checked | what it needs next | contributors |
|---|---|---|---|
| Erdős #306 The claimed solution of Erdős Problem #306 (sums of unit fractions with semiprime denominators) Rests on an arXiv paper and a Lean development, built on an earlier conditional Lean development by another author. | Reading guide written 2 certified, 0 accepted · 2 open | Do the formal statements say what the problem asks? a machine comparison of the claimant's main theorem with the third-party formal statement in google-deepmind/formal-conjectures, then a human read of any difference | Nervous Machine last cycle 14 Nov 2026 |
| Erdős #768 The claimed solution of Erdős Problem #768 (density of integers with a witness divisor for every prime factor) Rests on an arXiv paper and a Lean development that vendors two other Lean projects. | Reading guide written 1 certified, 0 accepted · 2 open | Do the formal statements say what the problem asks? two independent mathematicians read the formal statement against the problem as posed and sign, or refuse | Nervous Machine last cycle 14 Nov 2026 |
| Prime gaps ≤ 186 (OpenAI) The claim that primes come within 186 of each other infinitely often Rests on a Lean formalization with three stated assumptions, a numerical certificate (Python/FLINT) and a paper. | Reading guide written 5 certified, 5 accepted · 3 open | Do the formal statements say what a mathematician means? a number theorist reads the definitional trace against the formal file and the paper and signs its checklist | Fredrik Prüzelius last cycle 14 Nov 2026 |
| Prime gaps ≤ 240 (Zhang) The claim that primes come within 240 of each other infinitely often (Zhang) Rests on an exact arithmetic certificate (Python) and a paper. | Checks rerun 3 certified, 1 accepted · 3 open | The analytic argument has no formal deduction and no referee report a referee report or an independent expert read of the analytic sections | Nervous Machine last cycle 8 Nov 2026 |
| Erdős #1133 The claimed solution of Erdős Problem #1133 (polynomials agreeing with bounded data at most nodes) Rests on a PDF write-up in a public repository; no formal deduction. | Registered 0 certified, 0 accepted · 2 open | No formal deduction exists for the claimed proof a Lean formalization of the main theorem, by the claimant or anyone else, with the statement written by a third party | no contributions last cycle 29 Apr 2026 |
| Erdős #1061 The claimed solution of Erdős Problem #1061 (solutions of sigma(a) + sigma(b) = sigma(a+b)) Rests on an arXiv paper only; no formal deduction. | Registered 0 certified, 0 accepted · 2 open | No formal deduction exists for the claimed proof a Lean formalization of the main theorem, by the claimant or anyone else, with the statement written by a third party | no contributions last cycle 24 Jun 2026 |
| Erdős #856 The claimed solution of Erdős Problem #856 (sets with no k elements sharing a pairwise least common multiple) Rests on an Overleaf read-only document; no fixed file and no formal deduction. | Registered 0 certified, 0 accepted · 3 open | No formal deduction exists for the claimed proof a Lean formalization of the main theorem, by the claimant or anyone else, with the statement written by a third party | no contributions last cycle 15 Apr 2026 |
| Erdős #550 The claimed solution of Erdős Problem #550 (Ramsey numbers of trees versus complete multipartite graphs) Rests on an arXiv paper and a Lean development. | Registered 0 certified, 0 accepted · 3 open | The Lean development has not been built or kernel-checked by anyone outside the claimant a pre-registered rerun: fetch at the pinned commit, build, confirm no sorry or admit, print the axioms | no contributions last cycle 22 Jun 2026 |
| Erdős #1177 The claimed solution of Erdős Problem #1177 (three statements about triple systems avoiding a fixed finite one) Rests on an arXiv paper and a Lean development shared with the claim on problem 593. | Registered 0 certified, 0 accepted · 3 open | The Lean development has not been built or kernel-checked by anyone outside the claimant a pre-registered rerun: fetch at the pinned commit, build, confirm no sorry or admit, print the axioms | no contributions last cycle 23 Jun 2026 |
| Erdős #671 The claimed solution of Erdős Problem #671 (Lagrange interpolation and the Lebesgue function) Rests on two written arguments and two Lean files, one pinned by hash and one a live-editor link. | Registered 0 certified, 0 accepted · 4 open | The Lean development has not been built or kernel-checked by anyone outside the claimant a pre-registered rerun: fetch at the pinned commit, build, confirm no sorry or admit, print the axioms | no contributions last cycle 22 Jun 2026 |
| Erdős #593 The claimed solutions of Erdős Problem #593 (finite triple systems forced by uncountable chromatic number) Rests on two independent arXiv or PDF write-ups and two Lean developments, one per claimant. | Registered 0 certified, 0 accepted · 4 open | The Lean development has not been built or kernel-checked by anyone outside the claimant a pre-registered rerun: fetch at the pinned commit, build, confirm no sorry or admit, print the axioms | no contributions last cycle 23 Jun 2026 |
| Erdős #731 The claimed solution of Erdős Problem #731 (the least non-divisor of the central binomial coefficient) Rests on an arXiv paper and a Lean development, under the claimant's own formalisation of the word 'reasonable'. | Registered 0 certified, 0 accepted · 4 open | The Lean development has not been built or kernel-checked by anyone outside the claimant a pre-registered rerun: fetch at the pinned commit, build, confirm no sorry or admit, print the axioms | no contributions last cycle 27 Jun 2026 |