Olympiad golds, Erdős problems, a disproved 87-year-old conjecture and a better Riemann bound. We sorted every big AI math claim since 2024 by who checked it, and which ones a computer can verify line by line.
Every few weeks a post says AI just solved a famous math problem. Some of those posts are right. Some describe a real result in words that are much bigger than the result. Our own breakdown of Claude's Riemann zeta result and why it isn't a Riemann Hypothesis proof is the most-read page on this site, so the question clearly matters to people.
This piece is the wider version. I went back to the primary source for each claim: the lab's own post or paper, the Erdős problem database, Epoch AI's benchmark data, and Terence Tao's blog. For each result I noted the date, who checked it, and whether a machine-checkable proof exists. We read these sources on 3 and 4 October 2026. We didn't check any proof ourselves.
The scorecard: twelve claims and who checked them
Twelve AI math results since 2024 hold up on their primary sources. Three were checked by people outside the lab that made them. Eight come with a published Lean proof. Two rest mainly on the lab's own word, with the work published for anyone to inspect.
Twelve AI math results, 2024 to 2026, by who checked them. Read on primary sources, 3 to 4 October 2026. · aliteq research
What each claim is, in one line
IMO 2025 gold, 35 of 42
Date
21 Jul 2025
Lab
Google DeepMind
Verdict
Real. Graded by IMO coordinators
Erdős
Date
20 May 2026
Lab
OpenAI
Verdict
Real. Lean-verified, written up by nine mathematicians
AI olympiad gold is real. Google DeepMind's Gemini Deep Think scored 35 of 42 at IMO 2025, and IMO coordinators graded it. One year earlier, AlphaProof needed humans to translate the problems and two to three days of computing. By 2026, Axiom Math reports a perfect 42 of 42 in Lean.
Here is the sequence on the labs' own pages:
IMO 2024. Google DeepMind says AlphaProof and AlphaGeometry 2 solved four of six problems for 28 points, silver-medal standard. Experts first translated the problems into formal languages such as Lean, and it took two to three days of computation.
IMO 2025, Google DeepMind. Gemini Deep Think solved five of six problems perfectly for 35 of 42, in plain English, "within the 4.5-hour competition time limit". DeepMind says it was among "an inaugural cohort to have our model results officially graded and certified by IMO coordinators". The post quotes IMO President Gregor Dolinar: "We can confirm that Google DeepMind has reached the much-desired milestone, earning 35 out of a possible 42 points — a gold medal score."
IMO 2025, OpenAI. On 19 July 2025, OpenAI researcher Alexander Wei posted that an experimental reasoning model "has achieved ... gold medal-level performance". The proofs are public on GitHub. We couldn't find the grading details on a primary page we could read, so we count it as self-reported.
IMO 2025, Harmonic. Its Aristotle model reached "Gold Medal-level performance", with every solution "formally verified ... using the Lean4 proof assistant".
IMO 2026, Axiom Math. The AxiomProver repository says it "solved all six problems, achieving a perfect score of 42/42", with Lean statements and proofs for each. Its own timings add up to 1,496 minutes, about 25 hours, and the longest problem took 869 minutes.
Other labs also reported perfect 2026 scores. We didn't find an IMO page listing AI results, so they aren't on our card. One caveat applies to all of this. Olympiad problems are hard, but each one has a known solution that a strong teenager can find in a few hours. That makes them a test, not research.
Erdős problems: real wins, plus a lot of noise
AI has settled real Erdős problems, and several of the results are verified in Lean. The best-known is OpenAI's disproof of the 1946 unit distance conjecture in May 2026. But the same sweeps also produce many wrong or already-known answers. Google DeepMind's own paper says so in plain numbers.
Paul Erdős left hundreds of open questions, many with small cash prizes. The Erdős Problems database run by Thomas Bloom lists 1,221 of them, of which 586 (48%) are solved. Several entries now carry an AI credit:
#90, the unit distance conjecture. Marked "DISPROVED (LEAN)": "disproved by an internal model at OpenAI". Erdős dated it to 1946. Nine mathematicians, Bloom among them, posted "a short, digested, human-verified version" of the argument on arXiv on 20 May 2026.
#1051. Marked "PROVED (LEAN)", "solved in the affirmative by Aletheia", Google DeepMind's math agent built on Gemini Deep Think.
#619. Marked "SOLVED (LEAN)", "resolved in the negative by Claude Fable 5 (prompted by Kuhn)". The community wiki dates it to 9 June 2026.
#728. Marked "PROVED (LEAN)". The page credits Kevin Barreto and ChatGPT-5.2 and notes that the question as written was ambiguous. The result "appears to answer the question in the spirit it was intended".
Now the noise. In December 2025, Google DeepMind pointed Aletheia at 700 problems marked open. Its own paper reports the funnel.
Aletheia's December 2025 sweep, from Google DeepMind's own paper, and the community tally of AI-only attempts to 30 June 2026. · aliteq research
Of 200 graded answers, 137 (68.5%) were "fundamentally flawed" and 63 were technically correct. Only 13 answered the problem Erdős actually meant. Of those, 8 were already solved in the literature and 5 were "seemingly novel". The authors conclude that the open status of many problems "was through obscurity rather than difficulty". They also warn of "subconscious plagiarism": a model reproducing a result it absorbed in training without saying where it came from. And they add a line every Lean fan should read: "formal verification cannot help with any of these difficulties."
The community wiki in Terence Tao's erdosproblems GitHub repository tells a similar story. It stopped updating on 30 June 2026. Its "AI standalone" section lists 61 attempts with no significant human help. We counted 19 full solutions (6 with Lean), 23 partial or variant results, 10 incorrect and 9 unverified. The wiki's own first disclaimer is "This page is not a benchmark".
Famous conjectures: two disproofs and a bound
The biggest 2026 results are a disproof of the Jacobian conjecture, OpenAI's ten-result paper and Claude's Riemann zeta bound. The first two settle questions outright. The third is a real improvement on a related problem, and Anthropic says plainly that it won't lead to a proof of the Riemann Hypothesis.
The Jacobian conjecture (1939). It said a certain kind of polynomial map that is reversible near every point must be reversible everywhere. On 19 July 2026 (US time), Anthropic mathematician Levent Alpöge posted "the jacobian conjecture is false" on X, with an explicit three-variable map and thanks to "fable". A later arXiv paper by Arno van den Essen says it was found using "Anthropic's AI model Claude Fable 5, which was released on June 9, 2026". Terence Tao wrote it up two days later, noting it was found "using the Fable AI". He called checking it "an extremely quick verification". A counterexample is the easiest kind of result to check: you plug the map in and do the algebra. We found no published Lean proof for it, so we don't claim one.
OpenAI's ten results (August 2026). A 253-page paper presents "results obtained by an internal OpenAI model". They include a non-sofic group, a counterexample to Connes's rigidity conjecture and Erdős problems #146 and #183. The Lean files are public in the openai/ten-proofs repository. The Erdős database marks both of those problems as Lean-verified. Our news piece on OpenAI's ten proofs covers the announcement.
The Riemann zeta bound (10 August 2026). An unreleased research version of Claude raised the proven share of zeta zeros on the critical line from 41.6% to 67.2%. Anthropic says it used two sessions in Claude Code and 31 million output tokens. First came 650 ideas that failed, then about 60 subagents over a day and a half. Two Anthropic mathematicians, Levent Alpöge and Ralph Furman, validated it. Two outside experts, Brian Conrey and Dan Goldston, examined it. A Lean version passes the standard checker. The full story, and why this is not the Riemann Hypothesis, is in our Riemann explainer.
Hadamard matrix of order 668. Epoch AI's Open Problems page lists it as "Solved (human + AI)", "crediting a team of three humans and Claude". The answer fills every open order up to 2000. A matrix like this can be checked by computer in seconds. Our Hadamard news piece has the backstory.
Benchmarks: answer keys are done, open problems are not
On math tests with a known answer, the best AI now scores close to 100%. On genuinely open problems the numbers collapse. Epoch AI's own data shows 18.4% of its listed open problems solved with any AI help, and 2.9% of its hardest Erdős set.
Best score so far on Epoch AI's math tests. Epoch benchmark data, read 4 October 2026. · aliteq research
FrontierMath is Epoch AI's set of unpublished, very hard problems with known answers, and OpenAI funds it. Epoch released a corrected version 2 on 12 June 2026, fixing errors in 42% of problems. On the new Tier 4, its research-level set, GPT-6.1 Sol scored 100% on 29 September 2026. On 10 September, Epoch wrote that "every FrontierMath Tier 4 problem has now been solved by AI", and that mathematicians "often commented that AI found unintended shortcuts".
Two newer Epoch sets test the real thing:
Open Problems. Unsolved problems "that have resisted serious attempts by professional mathematicians", with answers a computer can verify. Of 49 listed, 4 are solved by AI and 5 by humans with AI. Forty are unsolved.
FrontierMath Erdős. 68 Erdős problems that were open in August 2026, chosen with Thomas Bloom as especially hard, where the model must write a full Lean proof. GPT-6 Astra scores 2.9%, which is 2 problems by our math. Four other models tested score zero.
So a perfect benchmark score tells you the model is very good at problems someone has already solved. It doesn't tell you it can do research. If you want the background on why these models spend so long "thinking" first, see what a reasoning model is.
How to read the next "AI solved it" headline
A math claim is only as strong as its checking. A Lean proof checks the logic, people check that it is the right question and that it is new, and a self-reported score checks nothing. Five questions sort most headlines in a minute.
Find the primary source: the lab's post, the paper, or the problem's own page. A screenshot of a tweet about a tweet doesn't count.
Look for a Lean proof. If there is one, the logic is machine-checked. If not, someone has to read every line.
Check who outside the lab looked at it. Named outside mathematicians and the problem database count. 'Experts' with no names don't.
Ask whether it answers the intended question. Aletheia's 63 technically correct answers shrank to 13 on this test alone.
Check the literature date. Many 'new' Erdős solutions turned out to be decades old, which is why the wiki has a literature-search section.
That last step is where most of the 2025 hype came from. The AI wiki logs 84 cases where a model found an existing answer in the literature, starting in late September 2025. Finding a forgotten paper is useful. It isn't the same as solving the problem.
What's still hype
The Riemann Hypothesis is still open. Nothing on this list proves it, and Anthropic says its technique won't. The broader pattern is that AI has moved from "can't do olympiad math" to "settles some real open problems" in about two years, but the solved ones skew toward questions that turned out to be obscure rather than deep.
Three claims I'd treat with care right now:
"AI solved a famous problem" when the result is a bound, a special case or a variant. The zeta result is a 67.2% bound, not 100%.
"Gold medal" scores the lab graded itself. They may be right. They are still not the same as IMO coordinators grading the work.
Benchmark records as proof of research ability. Tier 4 is saturated; Epoch's Lean Erdős set sits at 2 of 68.
What's real is also real. A machine-checked disproof of an 80-year-old Erdős conjecture, and a counterexample to the Jacobian conjecture that mathematicians could check by hand, would have sounded like science fiction in 2024. If you landed here from our Riemann zeta explainer, that result belongs in the same "real, checked, and smaller than the headline" column as most of this list.
Quick answers
Has AI solved the Riemann Hypothesis?
No. In August 2026 an unreleased version of Claude raised the proven share of Riemann zeta zeros on the critical line from 41.6% to 67.2%. The hypothesis needs 100%, and Anthropic says it doesn't expect the technique to lead to a proof.
What is the biggest math problem AI has actually solved?
The strongest cases are OpenAI's May 2026 disproof of Erdős's 1946 unit distance conjecture, which is Lean-verified and written up by nine mathematicians, and the July 2026 counterexample to the 1939 Jacobian conjecture that Levent Alpöge found with Claude Fable 5.
Did AI really win gold at the International Math Olympiad?
Yes. Google DeepMind's Gemini Deep Think scored 35 of 42 at IMO 2025, graded by IMO coordinators. OpenAI and Harmonic also reported gold-level results that year, and Axiom Math reports 42 of 42 at IMO 2026 with Lean proofs.
How many Erdős problems has AI solved?
There is no official count. The community AI wiki logged 61 AI-only attempts to 30 June 2026, with 19 full solutions, 6 of them in Lean. Many more involved humans working with AI. The database lists 1,221 problems, 586 of them solved by anyone.
What does it mean when a proof is verified in Lean?
Lean is a programming language for mathematics. A proof written in it is checked step by step by a small trusted program, so the logic can't be wrong. It doesn't check that the question was stated correctly or that the result is new.
Are AI math benchmarks like FrontierMath solved?
The tiers with known answers are close to it. GPT-6.1 Sol scored 100% on FrontierMath Tier 4 in September 2026. On Epoch's set of 68 hard open Erdős problems requiring Lean proofs, the best model has 2.