OpenAI Says It Solved Three Erdős Problems. The Database Says Open.

本文另有中文版：OpenAI 說解掉三道 Erdős 難題，收錄它們的資料庫標的是還沒解決

Look up Erdős problem 183 on erdosproblems.com, then 146, then 180.

All three pages carry the same status line: OPEN (LEAN). All three report 0 claimed proofs for this problem — that was the state of the site on 2026-08-04.

Three days earlier, on 2026-08-01, OpenAI published a set of ten results and wrote that three of them resolve exactly those problems.

Nobody is saying the proofs are wrong.

The control group is on the same site: problem 90, the unit-distance counterexample from May 2026, carries the status DISPROVED (LEAN), and the site adds a line saying the problem was solved in the negative and the proof checked in Lean. On 183, 146 and 180, that same field reads No explanation available. The rulebook does hand out a solved verdict, and these three did not get one.

The gap extends one field further down, where problem 90 answers Yes under “Formalised statement?”; the three Erdős problems OpenAI names answer No, next to a standing invitation to create a formalisation. One database, one set of fields, and on one side even the statement has not been formalized yet.

None of this is a claim about whether the proofs hold. It is a status box that did not exist in June.

open (Lean) means a formal proof of the problem exists, a machine accepts it, and no human has yet read it closely enough to accept it; by this database’s rules, the problem stays open.

What got automated is the proof. What did not get automated is the understanding. And the database that catalogues these three problems reserves the word solved for the second one.

The status was added on July 26, and the first problem to get it was #1112

The database behind erdosproblems.com lives on GitHub and is maintained by Terence Tao, professor of mathematics at the University of California, Los Angeles. As of 2026-08-04 its README counted 210 problems with a solution formalized in Lean, and stated the rule plainly: this set need not be a subset of the solved problems, because “a formalized solution that has not yet been digested by a human reader” keeps its informal status.

That rule is new.

On 2026-07-26 at 19:12 UTC, Tao explained the design on Mathstodon. The reason he gave: AI-generated proofs that have been formalized in Lean but not digested enough for a human expert to accept them are a phenomenon likely to persist, so the database now decouples a problem’s formal status from its informal status. The inaugural case was #1112 — a verifiable formal solution exists, nobody has digested it, and in the informal sense the problem is still open. His post ended with a forecast: “This problem will likely soon be joined by many others.”

Six days later, OpenAI published, and three problems joined.

The box is still nearly empty: a scan of the full status table as of 2026-08-04 finds four problems marked open (Lean), namely #1112 plus #146, #180 and #183. The same table shows 604 open, 210 proved, 120 proved (Lean), 63 disproved (Lean) and 23 solved (Lean). Tao’s first case and OpenAI’s three are the entire population of this status.

The site’s rules were not written with AI in mind, either. The forum on erdosproblems.com is governed by rules set by its owner, Thomas Bloom, Royal Society University Research Fellow at the University of Manchester. They state that the site does not exist as a benchmark for AI progress and that every mathematical claim must be independently verified by a human before it is posted. The last rule is a single sentence: “If you do not understand the mathematics yourself, please do not post it here.”

The ten proofs are the most checkable thing in the announcement

Start with the layer that can be inspected, because it is unusually solid for an AI claim.

The release was not just a blog post: it came with a 249-page paper, a GitHub repository, a separate PDF narrating the model’s reasoning, and a named post from an OpenAI employee. The repository is openai/ten-proofs, Apache-2.0, publicly readable, created 2026-08-01 at 06:10 UTC, and anyone can download it and re-run it.

Inside are ten .lean files, plus a formalization.yaml that registers 12 main results. Each entry lists the theorem’s full declaration name, the file it lives in, its sorry count, and the axioms it depends on. In Lean, sorry is a placeholder meaning “skipped for now” — a proof containing one is not finished.

Across the ten solution files, the sorry count is 0 and the custom axiom count is 0.

The axiom column is equally clean, in that all 12 registered results use only propext, Classical.choice and Quot.sound, the three standard axioms of Lean’s logic. They are not extra assumptions bolted on for this occasion. The repository also ships a ComparatorChallenges/ directory with instructions to replay the proofs through the comparator tool and independently implemented checkers — the procedure the Lean documentation calls the Gold Standard. That is a much higher level of inspectability than an AI capability claim usually offers.

The paper states its own novelty claim in Chapter 3, whose related-work section lists earlier conditional routes to a non-sofic group — Bowen–Burton, Gohla–Thom and others — and notes that all of them depended on an unproved stability hypothesis. Then one sentence: “Theorem 1.1 requires no unproved stability hypothesis.” The same chapter marks the result’s limits without being asked: it does not determine whether the group in question is hyperlinear, a neighbouring approximation property.

One field deserves to be pulled out: the review section of formalization.yaml reads status: "agent-reviewed" — the review was done by an agent, and OpenAI labelled it that way itself. The blog is similarly direct about the division of labour: OpenAI says it helped prepare the manuscripts and formalize the proofs in Lean and takes responsibility for their correctness, while the mathematical arguments were generated by its system. There is also something that had not happened as of 2026-08-04: no arXiv preprint, no record of a journal or conference submission, and zero issues on the repository.

What Lean certifies, and what it hands back to you

A Lean-checked proof guarantees something very specific: under the definitions written down in these files, this statement follows.

It does not guarantee that those definitions match the concept the literature calls by that name.

This is not an outsider’s complaint — the Lean language reference makes the distinction itself, and its page on validating proofs says it is important to separate “does the theorem have a valid proof” from “what does the theorem statement mean.”

The same page goes further. It files un-reviewed AI-generated proofs and programs under malicious, a category the document defines as code that goes out of its way to trick or mislead the user, exploit bugs, or compromise the system. The check it prescribes is the one described above: run #print axioms on the theorem and confirm that only those three standard axioms come back. If sorryAx appears, the theorem or something it depends on used sorry or is incomplete.

The Gold Standard layer, the documentation notes, should only be necessary in high-risk scenarios, and it names three: proof marketplaces, high-reward proof competitions, unaligned AI. Even after running the whole procedure, five assumptions remain on the official list — the soundness of Lean’s logic, the correctness of the comparator plumbing, the security of the sandbox, the absence of an implementation bug affecting every checker at once, and the absence of human error or misleading presentation in the trusted challenge file.

One more instruction: if there is any doubt that a theorem means what it appears to mean, its statement and every definition it references must be investigated carefully, with particular attention to custom notation and type classes.

That instruction has a concrete referent in the non-sofic result. A group can be pictured as a set of elements plus a multiplication rule — laid flat, a multiplication table. A countable group is sofic if every finite piece of that table can be approximated by permutations of a finite set: multiplication has to hold at almost every point, and every non-identity element has to move almost every point. Gromov introduced the property in his work on symbolic dynamics; Weiss later named sofic groups and asked whether a non-sofic one exists.

The file ComparatorChallenges/D_NonSoficGroup.lean is 39 lines long and it imports Mathlib, but the four load-bearing definitions — normalizedHamming, PermutationModel, GoodOn and Sofic — are written inside that file rather than pulled from Mathlib. So what the machine certifies is that under these definitions, the statement is provable. Whether these definitions are faithful to the sofic of the literature is a human judgment.

Here is the part that is easy to get wrong. That 39-line challenge file does end in sorry — but it exists only to pin down the statement, and there the sorry belongs. In the actual solution file, NonSoficGroup.lean, sorry appears 0 times. Reading the challenge file’s sorry as a hole in OpenAI’s proof is reading the wrong file for the wrong purpose.

The size difference between the two files is worth a look. The challenge file is 39 lines and says what is to be proved; NonSoficGroup.lean is 34,440 lines and says how. The ten solution files come to 548,205 lines in total, from GapCVP.lean at 130,430 down to MulticolorTriangleRamsey.lean at 3,053. Nobody has read it yet stops being an abstraction in front of thirty-four thousand lines of Lean.

One more gap belongs in the record: the paper’s Theorem 1.1 says the unit group of the binary Leavitt algebra is not sofic — a specific group. The top-level Lean theorem says a finitely presented non-sofic group exists. The two are compatible, but they are not the same sentence.

Four days before the release, Lean’s kernel proved False

Theorem provers are not magic, and four days before this release there was a demonstration.

On 2026-07-28 at 03:28 UTC, leanprover/lean4 received issue #14576. The title, verbatim: “Kernel accepts wrong-structure projections, allowing an axiom-free proof of False.”

In formal verification, being able to prove False means the system will, at that moment, prove anything.

The issue closed the same day at 13:39 UTC, about ten hours later. Both halves matter: holes like this are real rather than hypothetical, and the response time is measured in hours.

The official residual risk — that no implementation bug affects every checker at once — is an assumption, not a guarantee. Independently implemented checkers are not immune either: a submission the same week reported a soundness bug in the checker nanoda and its derivatives.

That kernel bug has one traceable point of contact with this release. The lean-toolchain file in ten-proofs pins leanprover/lean4:v4.32.0, released 2026-07-13; v4.32.1 followed on 07-22. The fix for #14576 was merged on 07-28 at 13:39 UTC, and v4.32.2 carrying it shipped the same day at 16:34 UTC. The pinned version predates that fix by fifteen days and does not contain it.

That is where the sentence stops. Whether any of the ten proofs touch the construction the bug lived in, nobody has said, and this piece cannot determine it — this section is not an argument that the proofs are flawed. The point is a different one: you can ask that question and answer it yourself, because a version number is pinned in a public file. This layer is checkable; the layer above it is not.

Above the proofs, nothing is formalized

The checkable part ends here, and on the next layer Lean has no jurisdiction at all.

Start with the model: the name “Astra” appears 0 times in the 249-page paper and 0 times in the reasoning-narration PDF; throughout, the paper writes only an internal OpenAI model. The name shows up in two other places: once in the blog, where the results are attributed to an internal version of Astra, described as OpenAI’s next major model; and in the repository’s formalization.yaml, whose automation section records models: ["Astra (OpenAI)"] and framework: "Codex".

So the thing that produced these ten results is an unreleased internal model. There is no public product, no API and no model card, and what outsiders can inspect is its output.

The more interesting item is that two accounts went out the same day. The blog’s summary line says each of the ten results resolves or makes substantial progress on a long-standing open problem. On the same day, OpenAI’s Noam Brown wrote in a named post that an internal version of Astra had “solved 10 major open problems.”

The official page carries the hedge; the named post says ten solved. Same day, same organization.

The wording differs elsewhere in the same post, too: Brown wrote next major model family, the blog wrote next major model.

Then the count: “ten” is a packaging number, because formalization.yaml registers 12 main results, because item 10 contains two separate conjectures and item 2 covers two families of codes. Whether it is ten or twelve depends on how you count.

Then the number everyone quoted. OpenAI’s own sentence says the tokens needed to find solutions to these problems “would cost roughly $2,000 at Sol API rates,” and the sentence after it says those arguments were then prepared into manuscripts by humans using the same model.

There are three limits inside that sentence, and none of them is optional.

The first is would cost — conditional, a conversion rather than a bill. The second is at Sol API rates, which prices the work using the published rates of a different model, GPT-5.6 Sol; Astra has no published rate, because it has not been released. The third is that the figure covers only the tokens needed to find the solutions. It does not cover formalizing them, it does not cover the wall_time: "1 week" recorded in formalization.yaml, and it does not cover the human manuscript preparation named in the same paragraph.

“Ten hard problems for $2,000” strips out all three.

The word “first” also has to be handled problem by problem. The blog uses the word “first” 0 times, and describes the non-sofic result only as addressing a central open question in group theory. The 249-page paper uses “first” 178 times, and some of those are explicit priority claims: the sphere-packing chapter states this is the first improvement since 1978 to the general sphere-packing exponent, and another passage claims the first improvements to two high-dimensional exponents since 1977 and 1978. The accurate version, then: the blog does not say first; the paper does say first for the sphere-packing results; it does not say it for the non-sofic one.

Finally, the denominator.

How many problems Astra was pointed at, and how many it failed, OpenAI has not disclosed. How many unsuccessful attempts sit behind ten successful results is not knowable from outside.

And the hedge in the blog’s summary line is used exactly once. “Substantial progress” appears one time in the whole post, in that one sentence covering all ten results. The ten individual write-ups below it use different verbs — establishing, constructing, addressing, proves, improves, resolves — and at no point does OpenAI mark which results it counts as resolved and which as substantial progress.

OpenAI did not draw that line, so nobody outside can draw it either. This piece does not sort the ten results either. Nothing on this layer is formalized, and every dispute lands here.

October 2025: the error was in the claim, not in the proof

Nine months earlier, something differently shaped happened around the same database, and it is worth the comparison because the error sat somewhere else entirely.

The starting point was accurate: on 2025-10-12, Sebastien Bubeck, then at OpenAI, posted that “gpt5-pro is superhuman at literature search,” because it had found that Erdős problem #339 was in fact solved twenty years ago. The claim was that the model found a paper.

On 2025-10-17, Mark Sellke, assistant professor of statistics at Harvard University, quoted that post and wrote that they had found solutions to ten Erdős problems listed as open. His post later received an X Community Note: GPT-5 had not solved the problems, it had located existing published literature.

Five days carried it from a model that found a paper to ten problems listed as open being solved.

Bloom corrected it the same day, calling it a “dramatic misrepresentation.” His explanation: GPT-5 found existing references he personally had not known about, and a problem marked open only means he personally is unaware of a paper solving it.

That same day, Kevin Weil, then an OpenAI executive, publicly acknowledged that he had misunderstood the original post — “Still very cool, but not the right words” — and said he would delete his. Bubeck explained himself publicly the next day: he had deleted his post, had not meant to mislead anyone, and only solutions already present in the literature had been found. Both men corrected their own wording in public within the same week, and every link in that chain has a permanent public URL.

As of 2026-08-04, problem #339 is listed as PROVED, with a note crediting Hegyvári, Hennecart and Plagne in 2003. The episode also left a structural mark on the site, and the mark was still there in August 2026.

A Wayback Machine comparison shows that the open-problem pages carried no disclaimer in the 2025-09-18 snapshot and did carry one by 2025-12-09: the open status reflects the current belief of the site’s owner, there may be literature he is unaware of, and readers should do their own literature search before investing significant effort. That paragraph was still on the #183, #146 and #180 pages verbatim on 2026-08-04.

The same shape of error recurred in December 2025. Quanta Magazine reported that an undergraduate at the University of Cambridge posted a solution to Erdős problem #333 on the site, saying it might be the first case of an LLM autonomously resolving an Erdős problem; within hours another user pointed out that Erdős himself had settled it in a 1977 paper. His own words afterwards: “As someone who has fallen for this twice now, it’s quite gut-wrenching.”

In October 2025 the claim itself was wrong. In August 2026 the claim holds up, and the argument moved somewhere else.

The argument is about weight and credit, not correctness

As of 2026-08-04, no named mathematician can be found publicly arguing that these ten problems were already solved, that they do not count as open, or that the proofs have gaps. The objections on the record are about two other things: how much the results weigh, and who they belong to.

On the erdosproblems.com forum’s “AI Contributions 2” thread, one commenter points out that the significance OpenAI’s page asserts is the significance of the problems, not of the contributions — the two can come apart, and a relatively minor contribution to a major problem is possible. Another groups results 3, 4, 9 and 10 as counterexamples: they do settle the conjectures, but only in a technical sense, meaning the people who posed them guessed wrong. The same commenter breaks down the sphere-packing contribution and argues that the existing human work accounts for most of it.

On the same forum, result 7 draws a separate objection: that it may overlap a 2026 GapSVP breakthrough that OpenAI’s paper does not cite. As of 2026-08-04 that objection has no conclusive resolution, and can only be recorded as raised and unsettled.

There is also a named assessment, and it comes from the right person. Chris Peikert, Arthur W. Burks Professor of Computer Science and Engineering at the University of Michigan, Ann Arbor, works in lattice cryptography, and the closest vector problem in result 7 is his field.

What he described in public was a reversal: his first reaction, and other people’s, was that the paper is badly written, and then he said he had changed his mind. He spent more than an hour on the roughly one-page proof overview alone, called it dense and terse and short on helpful framing, but said all the key ideas are there and the body of the paper is quite readable. He also noted that the result’s quantitative parameters can be tightened. His verdict on the result itself: “original, elegant, and beautiful.”

An expert inside the field read his way into it and changed his assessment, with more than an hour in between. Reading takes time. That is precisely what the open (Lean) label is describing.

The credit dispute has a second half, also in the public files. formalization.yaml has a prior_work field listing two existing Sphere-Packing-Lean projects, and an acknowledgements field thanking the authors of that project. The forum argument that the existing human work accounts for most of the sphere-packing contribution and OpenAI’s own registration of prior work in the manifest are both true at the same time.

The paper handles one attribution question on its own initiative. Chapter 4’s acknowledgements state that during preparation the authors learned of independent and concurrent work by Shuoxing Zhou giving a counterexample to Connes’s rigidity conjecture, developed in part with the assistance of GPT-5.6 Sol.

Step back and the argument is not specific to these ten results. Noga Alon of Princeton University told Quanta Magazine that these models are changing dramatically the way mathematical research is done. In the same article, Bloom describes a different problem: hundred-page-plus papers produced with AI by people without a mathematical background are piling up, and no human has read them or is going to.

Tao’s slides for his 2026 ICM public lecture set out the same shape. The transition he describes is neutral: mathematics moves from an era of proof scarcity to an era of proof abundance. His worry is conditional. Without suitable policy and cultural changes, what he calls impedance mismatches — or proof indigestion — will emerge, and AI-generated proofs will accumulate waiting to be verified.

The institutional response already exists in the Leiden Declaration on AI and Mathematics, which was published 2026-06-02 and endorsed by the International Mathematical Union, showed 3,409 signatories on 2026-08-04. Its fourth listed threat reads: proper evaluation is “endangered if results are communicated through informal channels such as press releases or blog posts,” often without a research paper or the other disclosures scientific evaluation needs.

Two of its other clauses land directly on this case. Responsibility for the correctness of arguments and results stays exclusively with the human authors, and credit and responsibility belong to humans in the mathematical community rather than to automated systems. And current automated techniques can produce plausible but unreliable arguments — a hazard the declaration extends past informal arguments to formalizations, where the difficulty is the translation between computer-encoded and human presentations. OpenAI’s page, in its section on responsibility, mentions the declaration’s signers itself.

Timothy Gowers, the British mathematician and Fields medallist, wrote about the declaration on his blog on 2026-07-26. His central worry is not correctness but culture: “the possible destruction of mathematical culture,” in which the literature expands enormously without a corresponding community of human experts who share an understanding of it.

He also proposes an allocation rule: if one person gets an LLM to produce a solution in one shot and another does the work of digesting it and explaining it to others, the second should get most of the credit. Set that rule beside the open (Lean) label and they turn out to be describing the same thing.

A discipline is being asked what solved means

The news here is not the ten proofs.

It is the status box.

Those two words concede something that did not have to be conceded before: a problem can have a machine-checked proof and remain unsolved at the same time. Before 2026-07-26, the database had no slot that could hold both of those facts at once.

Whether the three proofs are correct, this piece does not know. Their sorry count is 0, their axioms are the three standard ones, and anyone can download them and re-run them — that is what the machine can say, and it has now said it. The rest has to come from people, and by the pages as they stood on 2026-08-04, people have not said it yet.

What got automated is the proof. What did not get automated is the understanding.

The database reserves solved for the understanding; the forum rules require you to understand the mathematics before you post it; the Leiden Declaration keeps responsibility for correctness with human authors. These are three different instruments governing three different things, and they point the same way.

Sources

• OpenAI, “Ten advances in mathematics and theoretical computer science”: https://openai.com/index/ten-advances-in-mathematics/
• Paper PDF (249 pages): https://cdn.openai.com/pdf/ten-proofs-oai.pdf
• Lean formalization repository openai/ten-proofs: https://github.com/openai/ten-proofs
• erdosproblems.com problem pages: https://www.erdosproblems.com/183 , https://www.erdosproblems.com/146 , https://www.erdosproblems.com/180 , https://www.erdosproblems.com/90
• erdosproblems database (README and status definitions): https://github.com/teorth/erdosproblems
• Terence Tao, Mathstodon post, 2026-07-26: https://mathstodon.xyz/@tao/116987866420438091
• erdosproblems.com forum rules: https://www.erdosproblems.com/forum
• erdosproblems.com forum, “AI Contributions 2” thread: https://www.erdosproblems.com/forum/thread/AI%20Contributions%202
• Lean Language Reference, “Validating Proofs”: https://lean-lang.org/doc/reference/latest/ValidatingProofs/
• Lean 4 issue #14576: https://github.com/leanprover/lean4/issues/14576
• Lean 4 fix PR #14577: https://github.com/leanprover/lean4/pull/14577
• Lean 4 v4.32.2 release: https://github.com/leanprover/lean4/releases/tag/v4.32.2
• Independent checker soundness bug submission: https://github.com/leanprover/lean-kernel-arena/pull/81
• Leiden Declaration on AI and Mathematics: https://leidendeclaration.ai/
• Timothy Gowers on the Leiden Declaration: https://gowers.wordpress.com/2026/07/26/thoughts-about-the-leiden-declaration/
• Terence Tao, ICM 2026 public lecture slides: https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.pdf
• Quanta Magazine (2026-08-03): https://www.quantamagazine.org/why-the-legendary-erdos-problems-are-falling-to-ai-20260803/
• Thomas Bloom’s personal site (title and affiliation): https://thomasbloom.org/
• Noam Brown, post of 2026-08-01: https://x.com/polynoamial/status/2083467194663571701
• Chris Peikert on result 7: https://x.com/ChrisPeikert/status/2083950931301802053
• Sebastien Bubeck, original post of 2025-10-12: https://x.com/SebastienBubeck/status/1977181716457701775
• Mark Sellke, post of 2025-10-17 (carries a Community Note): https://x.com/MarkSellke/status/1979226538059931886
• Thomas Bloom, correction of 2025-10-17: https://x.com/thomasfbloom/status/1979254235075059732
• Kevin Weil, correction of 2025-10-17: https://x.com/kevinweil/status/1979270343941591525
• Sebastien Bubeck, explanation of 2025-10-18: https://x.com/SebastienBubeck/status/1979539604522127746
• erdosproblems.com #183, snapshot of 2025-09-18: https://web.archive.org/web/20250918080659/https://www.erdosproblems.com/183
• erdosproblems.com #183, snapshot of 2025-12-09: https://web.archive.org/web/20251209143450/https://www.erdosproblems.com/183