OpenAI publishes 722 math manuscripts from an unreleased internal model, many with Lean-checked proofs
OpenAI's new openai/math GitHub repository holds 722 manuscripts grouped into 372 result families across 16 areas, from number theory and complexity theory to mathematical physics. OpenAI says the unreleased model was given about 4,000 open problems and spent roughly three hours of ChatGPT Pro-level thinking compute per result on average. Many of the proofs are formalized in Lean. Not every result is, and the company warns that the unformalized ones may contain errors. The release follows OpenAI's September announcement of a Lean-checked Navier-Stokes singularity proof from the same internal system. OpenAI says it followed advice from the Institute for Advanced Study's advisory group on mathematics and AI. The company also plans to fund workshops on AI-produced results and says it is working toward releasing the model. For builders, the takeaway is that long-horizon reasoning you can verify is maturing fast. Pairing model output with machine-checkable proofs is a pattern worth copying in any domain where correctness can be tested formally.
