mathematics
Epoch marks a claimed AI-assisted ζ(5) proof as solved, with public Lean code but no settled consensus News
Epoch lists its Apéry irrationality target as solved “human + AI” after a September preprint claimed ζ(5) is irrational and linked public Lean formalization, while independent mathematical review and the AI attribution remain unresolved.
OpenAI says an internal model resolved 100-plus math problems and asks an independent group to advise on disclosure News
OpenAI has claimed more than 100 long-standing mathematical results from a new internal model, but has published neither an itemized list nor the proofs for that batch.
GPT-6 Astra helps solve FrontierMath's first Major Advance problem News
Epoch lists a proof that every approval-based committee election has a core-stable committee as its first solved Major Advance problem, crediting GPT-6 Astra with the central idea in an interactive human-AI collaboration.
The Clay Institute says Navier-Stokes has 'apparently been settled', but names no solver and starts no prize clock News
The Clay Mathematics Institute said on 11 September 2026 that the Navier-Stokes Millennium Prize problem 'has apparently been settled', without naming OpenAI or anyone else, and its own rules mean no prize can be awarded until a solution is published in a qualifying outlet and survives at least two years of scrutiny.
Twenty-five Fields Medallists say AI companies and mathematics are 'severely misaligned' News
Twenty-five Fields Medal winners, including Terence Tao and Peter Scholze, signed a declaration on 11 September 2026 saying the AI industry's race to solve famous problems is harming mathematics, a day after OpenAI withdrew its sponsorship of a Caltech AI math hackathon following a separate open letter from mathematicians.
NVIDIA publishes the whole recipe behind an IMO gold score, weights and all News
NVIDIA researchers released the full training recipe, data, 1.12 TB checkpoints and submitted proofs behind a Nemotron system that scored 30 of 42 points at the 2026 International Mathematical Olympiad, above the gold cutoff, as marked by the olympiad's own graders, using natural language only with no formal prover or internet access.
OpenAI says it cannot rule out that user chats improved the model behind its proof News
In its 8 September write-up of the Navier-Stokes result, OpenAI stated that while no specific user data was accessed to solve the problem, it 'cannot rule out' that de-identified data from two mathematicians' use of its products helped improve its models - a sentence that has shifted the dispute from mathematical credit to data consent.
Terence Tao says AI is strip-mining mathematics' supply of good problems News
Terence Tao argues that fruitful open problems are being consumed in a non-renewable way by AI systems, that identifying a promising problem is now the scarce resource rather than solving one, and that the incentive to stop sharing research directions could reverse centuries of open science.
Terence Tao calls the AI-assisted fluid blowup proofs a breakthrough News
A day before OpenAI announced its Navier-Stokes result, Terence Tao wrote that the new AI-assisted proofs of finite-time blowup for three fluid equations are a breakthrough with a high likelihood of extending to Navier-Stokes.
OpenAI says an internal model resolved the Navier-Stokes Millennium Problem News
OpenAI published a proof, produced by about 10,000 coordinated AI agents over 88 hours, that three-dimensional fluid flow can break down in finite time, and released a machine-checked Lean formalization alongside it.
Buckmaster says OpenAI asked him to drop his Anthropic coauthor News
NYU mathematician Tristan Buckmaster published a signed account alleging OpenAI pressed him to remove his collaborator from authorship and told him going public would ruin his career; OpenAI's Sebastien Bubeck called the allegations false and inflammatory.
Discovery Loop gets ten AI-assisted circle-packing candidates accepted by Packomania News
Discovery Loop used Claude Fable 5.1 to revise a solver and produced ten circle-packing candidates accepted by Packomania in an eight-hour, $27.72 consumer-PC run.
Anthropic's Lean artifact formalizes Fermat's Last Theorem, not a new discovery News
A public Anthropic Lean repository contains a complete formalization of a classical Fermat's Last Theorem proof route, which mathematician Kevin Buzzard says compiles and checks.
Anthropic says Claude produced a complete Lean proof of Fermat's Last Theorem News
Anthropic says Claude worked largely autonomously for 11 days to produce a complete machine-checked Lean 4 proof of Fermat's Last Theorem, extending a long-running human formalization effort rather than independently rediscovering Wiles's mathematics.
Station agents found new math on five of twelve AlphaEvolve problems News
In an open-world environment where AI agents from different labs pick their own research directions without a coordinator, agents produced results novel to the literature on five of twelve construction problems, including a new 604-point kissing configuration in eleven dimensions.
Claude helped set two elliptic-curve rank records in four days News
A public leaderboard run by an NSF mathematics institute recorded new rank records for elliptic curves on August 20 and August 23, both credited to Claude working with mathematicians Levent Alpoge and Ava Howell.
A record elliptic curve now lists Claude as a collaborator News
The canonical public record page for elliptic curve ranks has added a 2026 entry at rank 30 or higher, publishing an explicit curve with 30 independent points, and the attribution credits Claude alongside two named researchers, though no primary source describes what the model actually did.
AlphaEvolve helped tighten the matrix multiplication exponent, and the proof was checked in exact arithmetic News
A new paper establishes a certified upper bound of 2.371177 on the matrix multiplication exponent, improving the previous best of 2.371339, by reformulating the core optimization problem and refining the resulting algorithm with DeepMind's AlphaEvolve.
Claude raised the zeta critical-line bound to 67.2 percent, and Anthropic published the proof News
An unreleased research version of Claude raised the proven lower bound on the fraction of Riemann zeta zeros lying on the critical line from 41.6 percent to 67.2 percent, and Anthropic published the paper and a machine-checked Lean proof on August 10.
An AI tightened a 70-year-old constant, and the paper says its judgment was the weak part News
A case study from seven researchers documents how an AI system helped tighten the best known bounds on the Grothendieck constant, and reports plainly that the system was strong at technical execution but weak at research judgment and at tracking where the work stood.
The viral Riemann result an AI supposedly proved is not in the literature News
A widely shared claim that Claude raised the proven fraction of Riemann zeta zeros on the critical line from 41.6 to 67.2 percent does not match any published result; the closest paper says the two-thirds figure follows only if an assumption nobody has removed can be removed.
Three Days On, Nobody Has Publicly Compiled OpenAI's Ten Proofs News
OpenAI's repository of Lean proofs for ten mathematics results has 434 stars and 39 forks but exactly one commit, no pull requests, and no issues, and no third party has published a build log showing the proofs check.
The non-sofic group is the one OpenAI claim a computer can check News
Chapter 3 of OpenAI's new manuscript claims to have constructed a non-sofic group, settling a long-open question, and ships roughly 34,000 lines of Lean code with no unproved placeholders so outsiders can verify it.
OpenAI publishes ten mathematics claims with Lean proofs and no named authors News
OpenAI released ten claimed advances in mathematics and theoretical computer science today, produced by an unreleased internal model it calls Astra, with a 249-page manuscript collection and machine-checkable proofs for every result.
Terence Tao says the bottleneck in AI-assisted mathematics is understanding, not proofs News
In an ICM public lecture, Terence Tao argues that AI and formal proof systems accelerate generating and verifying proofs but not explaining, reviewing or canonicalizing them, so correct results could pile up faster than the field can absorb them.
A newly minted Fields medalist says he is joining OpenAI's safety division News
Jacob Tsimerman, awarded a 2026 Fields Medal on July 23, told journalists the same day that he will soon start a position in OpenAI's safety division, according to AFP.
AI Helped Crack a Famous Math Conjecture, and Humans Verified It in Lean News
Mathematicians found an explicit counterexample disproving the Jacobian conjecture in three dimensions, checked partly with an AI chatbot and formalized in a Lean proof, while two other viral AI-math claims remain unverified.
AI is now solving hard math and physics problems faster than humans can formally check them News
A widening 'verification lag' is emerging as AI produces candidate solutions to hard problems faster than experts can formally verify them - physicist Yuji Tachikawa reports Fable cracked a six-month research blocker, while a GPT-5.6 Erdos claim circulates without peer review.
Terence Tao brought his 1999 Java applets back to life with an AI agent -- and it found bugs he never knew about News
Fields Medalist Terence Tao used an AI coding agent to port about two dozen of his 1999 Java math applets to JavaScript in hours, reporting that the agent found two pre-existing bugs he was unaware of while introducing only one minor bug of its own.
Mistral releases a lean, open model built for formal math proofs News
Leanstral 1.5 is a free, open model specialized for writing machine-checked mathematical proofs, using a design that keeps only a small slice of itself active at a time.
Station Tool
An open-source open-world environment where AI agents from different model families pursue a shared research goal with no coordinator, choosing directions and writing into a shared literature. Suited to tasks that are scorable and finish in about two hours. Needs model-provider API keys and the OpenAI Codex CLI.
OpenAI NavierStokesAndEuler Tool
The Apache-2.0 Lean 4 formalization accompanying OpenAI's Navier-Stokes and Euler blowup claims, building against Mathlib and including a directory set up for independent proof-checking.
Nemotron IMO 2026 checkpoints Tool
NVIDIA's released specialist checkpoints, training data, 200-problem benchmark and inference recipe behind an officially graded IMO 2026 gold-level score (30 of 42). Each checkpoint is a 1.12 TB download; the model card recommends at least eight B200 GPUs.
Leanstral 1.5 Tool
A free, open mixture-of-experts model specialized for writing machine-checked Lean 4 proofs and translating ordinary math into formal, verifiable form.
Lean comparator Tool
The Lean toolchain component used to independently check the formalization behind Anthropic's zeta-function result. Useful to anyone who wants machine-verified mathematics rather than a persuasive argument.
Formal Conjectures Tool
Google DeepMind's open Lean library of formally stated open mathematical conjectures, now the venue where the claimed Jacobian conjecture counterexample is being reviewed in public. A usable resource if you want machine-checkable statements of open problems rather than prose.
Elliptic Curve Rank Leaderboard Tool
An NSF-funded public record of high-rank elliptic curves, where every submission publishes its witness points, commentary and edit history, and offers a JSON endpoint so anyone can verify a claimed record independently.
Anthropic Fermat's Last Theorem Lean repository Tool
A public Lean codebase for Anthropic's formalization of a classical proof route for Fermat's Last Theorem.