SignalCapabilitySG-0018
OpenAI released hundreds of math results and Lean proofs from an unreleased internal model
OpenAI published a GitHub repository of math manuscripts and proof artifacts produced by an unreleased internal model. The repository lists 722 manuscripts in 372 families, which Gizmodo counted as 377 new results; it says many but not all have Lean proofs and warns that some unformalized results could have issues. OpenAI says the model was posed about 4,000 problems after its existing math evaluations saturated. On Sept. 29 an Institute for Advanced Study advisory group, AGMAI, had asked labs to stop testing advanced problems on proprietary models; OpenAI said AGMAI's advice informed how it shared the results.
Why it matters
Hundreds of claimed research results from one unreleased model point to a jump in sustained reasoning that outsiders cannot test, because the model is internal, and the volume may outrun expert checking. The release also shows a lab still evaluating on a proprietary model after a mathematicians' advisory group asked labs to stop.
Sources
Read the reporting
3 sources. Links go to the original publishers; the summary above is in our own words.
- primarySharing AI progress in mathematicsOpenAI · October 2026openai.com/index/sharing-ai-progress-in-mathematics
- newsOpenAI Dumps 377 New Math Results on GitHub, Publishes Hand-Wringing Blog PostGizmodo · Oct. 6, 2026gizmodo.com/openai-dumps-377-new-math-results-on-github-publishes-hand-wringing…
Signals
More from the news desk
Cite and share
Use this signal
Citation
Paperclip Index. “OpenAI released hundreds of math results and Lean proofs from an unreleased internal model.” Signal SG-0018. Reported Oct. 6, 2026; updated Oct. 7, 2026. https://paperclipindex.com/signal/SG-0018