OpenAI Says It Solved Three Erdős Problems. The Database Says OPEN (LEAN).
On 2026-08-01 OpenAI published ten results and said three of them resolve Erdős problems 183, 146 and 180. On 2026-08-04 all three were listed as OPEN (LEAN) on erdosproblems.com, a status added on 2026-07-26. It means a formal proof exists and a machine accepts it, while the database keeps the informal status open until human experts have digested the proof by its own standard. Four problems in the whole database carried it.
本文另有中文版：OpenAI 說解掉三道 Erdős 難題，資料庫卻標 OPEN (LEAN)：「解決」有兩種意思
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. So what does “solved” mean here? Two different questions are in play: whether a machine can check the proof, and whether this database records human digestion and acceptance by its own standard.
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.
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 human experts have not yet digested it to the point where the database accepts it; by this database’s rules, the problem’s informal status stays open.
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.”
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. Tao’s first case and OpenAI’s three are the entire population of this status.
The ten proofs are the most checkable thing in the announcement
The official formalization.yaml registers 12 main results and lists their declaration names, files, sorry counts and axioms. In Lean, sorry is a placeholder for an unfinished proof.
The manifest records sorry_count: 0 for each of its 12 main results. Those are values registered by the repository.
For those results, the manifest lists propext, Classical.choice and Quot.sound as the axioms. The distinction between a proof and the meaning of its statement still remains.
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.
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.”
Judgment: two meanings of solved
I think what is new here is not the ten proofs but 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 still be open by the database’s standard. Before 2026-07-26, the database had no slot that could hold both of those facts at once.
This article does not independently adjudicate the three proofs. The official manifest records zero sorry counts and three standard axioms; the database pages as of 2026-08-04 kept the informal status open. Those are different records, and neither substitutes for the other.
So “OpenAI solved three problems” and “the database says open” do not contradict each other. They answer two different questions. One corresponds to the Lean proofs OpenAI published. The other is this database’s record of human digestion and acceptance, which on that date kept the informal status open.
Sources
- OpenAI, Ten advances in mathematics and theoretical computer science: https://openai.com/index/ten-advances-in-mathematics/
- Official manifest and toolchain: https://github.com/openai/ten-proofs
- Erdős problem pages: https://www.erdosproblems.com/183 , https://www.erdosproblems.com/146 , https://www.erdosproblems.com/180 , https://www.erdosproblems.com/90
- Database README: https://github.com/teorth/erdosproblems
- Terence Tao, 26 July 2026: https://mathstodon.xyz/@tao/116987866420438091
- Lean, Validating Proofs: https://lean-lang.org/doc/reference/latest/ValidatingProofs/
Frequently asked questions
Did OpenAI actually solve Erdős problems 183, 146 and 180?
OpenAI’s page states that the ten results include resolving Erdős problems 183, 146 and 180, and it published downloadable, re-runnable Lean proofs. But as of 2026-08-04, all three problems were listed on erdosproblems.com as OPEN (LEAN), each page showing the field “0 claimed proofs”, which is a site field, not a statement that nobody claims a proof. That status is not an accusation that the proofs are wrong; this article does not infer correctness or incorrectness from the status alone. It means a formal proof exists and a machine accepts it, while the database does not yet record it as digested and accepted by a human expert. By that standard, the problems stay open.
What does the status open (Lean) mean?
It is a status added to the database behind erdosproblems.com on 2026-07-26. Its maintainer, Terence Tao, explained the design: to handle proofs that are AI-generated and formalized in Lean but not yet digested by a human expert, the database decoupled a problem’s formal status from its informal status. The README states the rule directly — a formalized solution that has not yet been digested by a human reader keeps its informal status. The first case was problem #1112. By 2026-08-04, the pages for OpenAI’s three Erdős problems also carried the label.
Can a Lean-verified proof still be wrong?
Yes, but not in the way most people picture. The Lean documentation separates two questions explicitly: does the theorem have a valid proof, and what does the theorem statement mean. The machine settles the first, and only under the definitions written in that file; whether those definitions are faithful to the concept in the literature is a human judgment.