An open record of the Erdős problems

On October 6, 2026, OpenAI published 722 mathematical manuscripts produced using an unreleased internal model. By our count, the release includes results on 40 Erdős problems, although its announcement does not mention Erdős by name. It claims complete solutions to 17 problems that erdosproblems.com had not listed as solved, along with new proofs of 6 solved problems and partial results on 17 more.

The release's headline claims lie elsewhere, beginning with a negative answer to Hilbert's tenth problem over the rationals. That result says no algorithm can decide whether a polynomial equation with integer coefficients has a rational solution. Another is a proof of the quasi-Riemann hypothesis: no Dirichlet L-function, the Riemann zeta function included, has a zero with real part above 7/8.

Much of the release can be checked by anyone who builds its library in Lean, a language in which a computer checks every step of a formal proof. That library of over 100,000 files formalizes about 42% of the release's "top-line results", by OpenAI's count. Of the 17 complete Erdős solutions, 12 came with Lean proofs of the full statement. We rebuilt those 12 proofs, used separate AI review sessions to check that each Lean statement says what the problem asks, and now list all 12 problems as solved.

A release of this size needs a record that tracks each problem, tying each result to the evidence behind it. Today we are opening erdosproblems.ai, a record of results on the Erdős problems, along with an open-source repository that includes our proof for Erdős Problem 809. In the coming weeks, we will publish our results on several other Erdős problems.

Changes at erdosproblems.com

The 40 problems take their numbers from erdosproblems.com, which Thomas Bloom has built and maintained since May 2023. Starting from just over 200 problems drawn from Erdős's papers and problem lists, he has grown the catalog to 1,221 problems. Each comes with sources, references, and his account of what is known. Bloom has often restated problems in a form easier to follow than Erdős's originals.

Erdős wrote more than 1,500 papers, many of which posed open problems. Bloom's aim, in his words, is to include "all of the interesting Erdős problems". In August 2025, he added a forum, whose more than 9,000 comments have led to new collaborations and papers. The site now has almost 2,000 registered users and receives between 10,000 and 25,000 unique visitors on a typical day.

Terence Tao's community database and Google DeepMind's formal-conjectures project are both organized around Bloom's numbering. We owe him a great deal, because our repository and site are built on his catalog.

On October 6, before OpenAI's release, Bloom announced changes to the site. He has paused new comments and proof claims on individual problems and stopped showing whether problems are open or solved. New results will be described without "credit-giving language", whoever found them. The site itself continues under his curation, with more weight on written expositions of proofs.

His reason is that the main public use of the site had become advertising AI-generated proofs, "often without any attempt to explain them". Unexplained solutions of this kind, he writes, are "displacing and discouraging those who are actually interested in the mathematics".

He writes that places to record such proofs "should exist" and that, "if managed responsibly, they can serve a useful role in the mathematical ecosystem". He does not want to run one himself and asks that any such place stay separate from a site that presents the questions.

The repository we began in September and erdosproblems.ai, the site built on it, are a place of this kind, run independently of erdosproblems.com and without Bloom's involvement. Our site shows each question beside its record of results, and every problem page links to Bloom's page for that question in its fuller context. We quote each statement as Bloom and his contributors wrote it, with credit to him, as Google DeepMind does in its formal-conjectures repository.

A place to record results

Each of the 1,221 problems has a page on erdosproblems.ai with its statement, references, discussion, proof claims, and standing as open, claimed, or solved. A fixed rule sets each problem's standing from the evidence in our repository, so a problem counts as solved only once an accepted claim settles it. We accept a claim on the evidence of a refereed publication, a documented acceptance from outside our project, or a Lean proof that we have built and audited. Nearly all acceptances of the second kind rest on Bloom's own account of the result on erdosproblems.com.

Signed-in readers can comment or submit a proof claim, which names its submitter, can list its contributors and the tools they used, and appears only after a moderator approves it. Approval neither confirms the proof nor changes the problem's standing, which only an accepted claim can do.

We compiled these records from every solution we could find as of October 2026. The sources we cite most often are the research literature, erdosproblems.com's remarks and archived proof claims, and Boris Alexeev's collection of Lean proofs. Others include formal-conjectures, OpenAI's release, the Palomar registry of formal proofs, the bounties that conjectures.io pays for Lean proofs, and Tao's community database.

We will register our Lean proofs on Palomar, as we did for Problem 809. Bloom has said he will link to formalizations registered there, so Palomar is also the most direct way for a result in our record to reach erdosproblems.com. We will also contribute corrections and links to Tao's database. We plan to extend the same approach to other collections of open problems at mathproblems.ai.

The erdos repository

The site is generated from the erdos repository, which we built using Fractal, our open-source hierarchical agent orchestration platform. We used a cloud-hosted version of Fractal that we will release later this month. The Erdős repository contains multiple wikis, which are deterministically indexed trees of Markdown with YAML frontmatter, readable in any editor. They are built with Plasma Wiki, our wiki implementation, which is also open-source on GitHub. Agents can work from the repository directly, starting from the indexes and opening only the pages a task needs.

The repository's library holds about 2,300 papers, filed by subject and linked from the problems they bear on. About 450 are held in full under open licenses, each as a PDF with a Markdown transcription. The other 1,850 or so are summarized in our own words, many with their main results extracted onto separate pages.

Each problem page links to a claim page for each claimant's result. The claim page records the result's authors, sources, scope, and evidence. Our theorems carry a verification tier, from 0 for the author's own record, through 1 for a failed refutation attempt, to 2 for a Lean proof with an audited statement. So far, the reviewers at tiers 1 and 2 have been AI sessions, each working in a context separate from the author's.

Erdős Problem 809

Problem 809 concerns graphs with n vertices and ⌊n²/4⌋ + 1 edges, one more than any graph without a triangle can have. It asks how few colors suffice to color the edges of some such graph so that every cycle of a fixed odd length is "rainbow", with no color repeated.

For triangles, three colors suffice however large n is, while five-cycles need about n/2, by a result of Erdős and Simonovits. Burr, Erdős, Graham, and Sós showed in 1989 that longer odd cycles need a fixed fraction of n² colors, and asked whether that fraction is 1/8.

In the notation of erdosproblems.com, the question is whether χ_S(n, ⌊n²/4⌋ + 1, C₂ₖ₊₁) ∼ n²/8 for every k ≥ 3, where ∼ means the ratio tends to 1. In other words, it asks whether two disjoint cliques sharing one palette, which use about one color for every two edges, are asymptotically the best construction.

Matija Bucić, Kaizhe Chen, and Jie Ma proved this in a March 2026 preprint for every odd cycle of length nine or more. Their proof passes through a formula that holds at every edge density above 1/4, where density means the number of edges divided by n².

We solved Problem 809 with a different argument for the seven-cycle, set out in our paper. It proves that χ_S(n, ⌊n²/4⌋ + 1, C₇) = n²/8 + o(n²), which, together with their theorem, answers the question for every k ≥ 3. The paper also shows that, for seven-cycles, their formula for longer cycles fails at every fixed density strictly between 1/4 and 1/2. This second result, which shows why their method cannot work unchanged for seven-cycles, has not yet been checked in Lean.

Lean's kernel checks our formal proof of the full statement for every k ≥ 3, which includes a formalization of Bucić, Chen, and Ma's argument. The proof uses only Lean's three standard axioms and proves a statement written using only Mathlib, Lean's community library of mathematics. The formalization is registered on Palomar, whose automated review compared its Lean statement with the English one, but no person outside Plasma has yet reviewed the proof. Under Jacob Parish's direction, we found the proof using Fractal with GPT-6 Astra and Claude Fable 5.1, and formalized it using GPT-6 Sol.

Mathematics as engineering

In his 1900 address on mathematical problems, David Hilbert wrote that "as long as a branch of science offers an abundance of problems, so long is it alive". His tenth problem, which asks about integer solutions, was answered negatively in 1970 by Matiyasevich, building on work of Davis, Putnam, and Robinson. OpenAI's release claims the same answer over the rationals, in a manuscript that does not yet have a Lean proof.

Hilbert also wrote that "every real advance goes hand in hand with the invention of sharper tools and simpler methods". Mathematics has always been engineering in this sense: the building of definitions, theorems, expositions, tables, and libraries that others can reuse. In 1159, John of Salisbury wrote that "Bernard of Chartres used to compare us to dwarfs perched on the shoulders of giants". Each tool that others can pick up and reuse raises those shoulders a little higher for whoever comes next. Whether a person or a model found it, a proof checked by Lean is mathematics of this kind, because others can verify it and build on its parts.

Some mathematicians worry that machine-made proofs will pile up unread in repositories that only machines consult, and also that fewer people will do the mathematics themselves. We think part of the answer is structure, by which we mean a shared record that keeps each result beside its sources, authors, tools, checks, and failed attempts. Such a record should serve people first, through paper summaries, transcriptions, and named contributors, with agents reading the same pages.

We propose the format of the erdos repository for this record and share the repository itself, with its library, verification records, and Lean proofs. The format builds on the QED Manifesto of 1994, Mathlib, formalization.yaml, and the blueprints that tie informal proofs to formal ones. Anyone can clone the repository from GitHub or report a result we have missed on the relevant problem page at erdosproblems.ai.