Agentic AI news, research notes, and industry analysis.
Tag
11 stories in this tag.
OpenAI posted 372 AI-generated math proofs to GitHub — Lean-checked and likely correct, covering problems from the 4D Kakeya conjecture to progress on the Riemann hypothesis. Terence Tao says this marks the end of "Math 1.0" and calls for a rethinking of what mathematics is for in the age of AI.
Read more →Over 600 mathematicians responded to a survey on how AI labs should release AI-generated mathematical results. The resulting statement from AGMAI distinguishes proofs humans understand from those they don't — and places responsibility on labs to fund the gap.
Read more →A nine-member board of elite mathematicians — including Gowers, Hairer, and Witten — has formed at Princeton's IAS to advise OpenAI on releasing what it describes as "a large number of significant results in mathematics" produced by its internal model. The group is independent, unpaid, and publishing its recommendations publicly.
Read more →Twenty-five Fields Medalists — including Terence Tao, Pierre Deligne, and Peter Scholze — signed a declaration arguing that AI labs' race to solve famous mathematical problems is damaging the discipline. Their case: that problem-solving benchmarks are proxies for understanding, not understanding itself, and speed-running the proxy destroys the human transmission chain that makes mathematical knowledge actually useful.
Read more →OpenAI's agents proved that 3D Navier-Stokes equations can develop singularities — a genuine mathematical achievement. But the credit dispute that followed, involving an NYU mathematician and an Anthropic employee who'd been working the same problem for a year, raised a question that has no clean answer: what happens to independent research when an AI lab can decide to race at it the moment they hear a rumor?
Read more →Anthropic researcher and mathematician Levent Alpöge used Claude Fable during the World Cup final to produce a concrete, checkable counterexample to the Jacobian Conjecture — a problem on Smale's 1998 list of Mathematical Problems for the Next Century. The map is three polynomials in three variables. The Jacobian determinant is -2. The conjecture is false.
Read more →A UC Berkeley IEOR researcher used GPT-5.6 Sol Pro over two chat sessions totaling roughly four hours to prove a lower bound in zeroth-order convex optimization that had resisted attempts for 30 years, then formalized the result in Lean 4. A different kind of AI-does-math story than the CDC proof: one expert, one model, one hard problem.
Read more →OpenAI claims GPT-5.6 Sol Ultra produced a three-page proof of the Cycle Double Cover Conjecture — a 50-year-old open problem in graph theory — in under an hour, using 64 parallel subagents. The math community hasn't had a chance to stress-test it yet, and the details of how much human guidance went in are unclear. Worth watching, cautiously.
Read more →GPT-5.4 Pro solved Erdős Problem #1196 — a 1968 conjecture about primitive sets — when a 23-year-old amateur fed it the problem in a single prompt. The AI's approach used von Mangoldt weights and a downward Markov chain, a framing that existed in analytic number theory for ninety years but had never been applied here. Terence Tao's explanation for why experts missed it is the most telling part of the story.
Read more →In 2023, Terence Tao predicted that 2026-level AI would be a trustworthy co-author in mathematical research. This month he credited ChatGPT Pro with a proof in a real analysis paper — and published a philosophical essay arguing AI is a natural extension of humanity's tool-building tradition. Both together are a data point, not a verdict.
Read more →Donald Knuth published a paper in early March titled "Claude's Cycles" — named after the AI that spent an hour finding an algorithm for a directed graph decomposition problem he had been stuck on for weeks. Knuth wrote the formal proof himself; Claude did the search. Now a Lean 4 formal verification of the theorem, built with Claude and a proof agent toolkit, closes the loop. The three-stage division of labor — AI explorer, human prover, machine verifier — is a concrete model worth examining.
Read more →