OpenAI releases AI-generated mathematics with proofs for computer checking

OpenAI released mathematical research on October 6 produced by an internal AI model. The collection includes papers and Lean files that allow computers to check proofs. The company published the material in a public repository with procedures for revisions.

The release includes 10 accounts summarizing the model’s reasoning, information about attempted problems and estimates of computing resources. OpenAI said the average result required computation comparable to about three hours of reasoning through ChatGPT Pro. It plans to add more formalized proofs.

OpenAI consulted an independent mathematics and AI advisory group about publishing the work. The group said its involvement did not endorse the results or the process used to obtain them. It emphasized that mathematicians still need to assess and understand the findings.

OpenAI plans to fund meetings and research programs focused on understanding mathematics generated by AI. It also said it is preparing to release the model responsibly, but announced no release date.