OpenAI publishes new mathematical results with Lean proofs
A public repository brings together the results of an internal model, revision protocols and transparency information.
publication
Facts, analysis and limits
Verified facts
- Lean formalizations of many proofs.
- Ten summaries of reasoning and statistics of attempts.
- The model that produced these results is not presented as commercially available.
- The repository provides revision and citation protocols; OpenAI says it consulted the independent AGMAI group at the Institute for Advanced Study.
- OpenAI estimates the average calculation per result at about three hours of ChatGPT Pro reflection; this is neither a human working time nor an API price.
What changes
The publication moves the bottleneck towards reading, checking and disseminating results; abundant production does not amount to scientific consensus.
Practical implication
Distinguish a formalized proof, a result still subject to revision and community validation before describing an established discovery.
Availability
Public repository and proofs; the internal model remains unpublished. No new model offering is announced for Belgium/EEA.
Limits and uncertainty
Do not attribute these results to a specific public model or repeat a September scientific announcement as new. Formal proof verification does not replace human review of novelty, the theorem's scope and its presentation.