OpenAI says an internal AI model made headway on open problems in mathematics, and the company is posting the proofs online.
In a short announcement, OpenAI says a frontier model not yet released publicly produced new results on unsolved math problems. The company says it is sharing Lean proof formalizations, the formal language mathematicians use to machine check a proof line by line, along with other research details on GitHub. The post does not name the problems, say how many were solved, or link to the specific repository, paper, or commit a reader could actually check. No mathematician outside OpenAI is quoted confirming any of it.
That gap matters because AI math claims have a track record of outrunning scrutiny. Google DeepMind's AlphaProof made waves in 2024 with near gold medal performance at the International Mathematical Olympiad, and OpenAI itself claimed gold medal level results on this year's olympiad. Each time, the announcement comes first and the checking comes later, if at all.
Until independent mathematicians can actually open the Lean files and verify them, this is a claim, not a result.