OpenAI Publishes 722 Mathematical Manuscripts from an Unannounced Model

OpenAI published an open repository on GitHub containing 722 mathematical manuscripts distributed across 372 research families, produced by an unannounced internal company model. Around 4,000 problems were posed during the evaluation, with each result taking an average of three hours of reasoning compute via ChatGPT Pro using that model.

The repository included explicitly named results, including a zero-free region in the Riemann zeta function and a proof of the Hodge conjecture for CM abelian varieties. The company noted that the Riemann zeta manuscript underwent human editing to improve readability, and that some results departed from the general procedure used to generate the remaining manuscripts.

OpenAI warned that the results are in varying stages of verification, and that not everything published is formalized in the Lean automated theorem proving language, stating that "some unformalized results may contain issues," and that it will address any feedback promptly. The repository includes directories for formal proofs, reasoning traces, and a list of official verifications.

The release reopens the debate over the role of artificial intelligence in mathematics: while supporters argue it accelerates the discovery of proofs, skeptics emphasize that the absence of full automated verification leaves judging the validity of the results an open question requiring extensive human review.

What Do These Terms Mean?

Riemann Zeta Function: A pivotal mathematical function in number theory. The famous Riemann hypothesis is built upon it, and any progress in understanding its zeros is considered a major breakthrough in mathematics.

Hodge Conjecture: One of the hardest open problems in modern mathematics, asking about the relationship between complex geometric shapes and algebraic subvarieties within them. Its solution remains unknown.

Lean: A programming language and automated proof assistant for proving mathematical theorems step-by-step, allowing a computer to verify the proof's validity, making it stronger than human review alone.