Skip to content
Vibe Math Lab.

News

AI and mathematics in the news

AI systems are now producing math results, and the question is the one you face with any AI output: what has actually been checked? Each item below says what was claimed, what had been checked by its date, and who disputes what, with people quoted and linked to their sources. Each also has a short note with my own view. Lean, which comes up in all three, is a programming language for proofs: a computer checks each step, but only of the statement as written in Lean, and only if nothing in the file is left unproved (a placeholder called sorry) or assumed without proof (an extra axiom).

OpenAI’s October 6 release of 722 AI-written math manuscripts makes claims on 25 problems posed by the mathematician Paul Erdős, according to Thomas Bloom, who runs the Erdős problems database. OpenAI supplied Lean files for 21 of them. Bloom has not yet checked whether those files compile or state the right problems, and calls the results claims for now, though he expects most to be correct.

ResearchReported October 6, 2026; updated October 7

OpenAI releases 722 math manuscripts written by an unreleased AI model

OpenAI posted 722 math manuscripts, grouped into 372 families of related results, produced by an internal AI model it has not released. A day later it withdrew three after a sign error and revised fourteen more. By OpenAI’s own count, 300 of the remaining 719 manuscripts have their main result formalized in Lean (about 42%); the sources here report no outside check of those files. Mathematicians quoted here raised different concerns: one about verification, one about openness.

ResearchReported September 8 and 9, 2026

OpenAI says its AI agents solved the Navier-Stokes problem, a $1 million prize question about fluid flow

OpenAI announced that about 10,000 AI agents working together had solved the Navier-Stokes problem, one of seven math problems with a $1 million prize, by showing that the equations for fluid flow can break down. OpenAI says the proof is checked in Lean; neither news report mentions anyone outside OpenAI checking it. Terence Tao used the moment to warn about how AI is changing mathematics, and a mathematician who was working on the same problem has made allegations about credit that are still unresolved.