OpenAI posts more than 700 AI-written maths manuscripts
OpenAI published hundreds of manuscripts from an unreleased model on 6 October. Roughly 42% of the headline results have Lean formalisations, and mathematicians disagree about how to check the rest.
Source published · In the Daily Brief of 12 October 2026
Filed under Mathematics, Large language models, AI industry
OpenAI put a public repository online on 6 October containing manuscripts produced by an internal model that has not been released. The repository lists 719 manuscripts grouped into 372 families, each family being a principal result with its consequences. Press coverage gives slightly different counts, around 722.
According to the repository, about 42% of the top-line results have been formalised in the Lean proof assistant, and abridged reasoning summaries are provided for 10 families. A Lean check confirms that a proof follows from its stated assumptions. It does not confirm that the statement formalised is the one the authors meant, and that gap is central to the dispute.
Nature reported on 7 October that the release drew a sharp reaction. Some mathematicians welcomed solutions to long-standing problems. Others objected to receiving hundreds of results at once, outside the usual preprint and refereeing routes, and to the lack of consultation with the community.