The release of 6 October
OpenAI announced mathematical results from an internal model and published materials on GitHub. The company is also sharing Lean formalizations of many proofs and information about the research process. This gives discussion concrete artifacts to examine rather than only a capability demonstration.
What the repository says
The openai/math README explicitly states that the materials are at different verification stages. Not all have Lean formalizations, and unformalized results may contain issues. At the time of our check, the catalogue listed 719 manuscripts organized into 372 families and approximately 42% of top-line results formalized. These figures describe the current collection and may change.
Our editorial perspective
An accessible manuscript and a checkable formal artifact provide different levels of evidence. We therefore do not describe the entire collection as conclusively verified. Evaluating an individual result requires examining its statement, assumptions and specific checks. The announcement also does not, by itself, establish that the same internal model is available in an ordinary ChatGPT account.
