OpenAI published new results on open problems in mathematics from an internal frontier model and shared Lean proof formalizations and research details on GitHub.
A four-person team led by UC San Diego professor Ben Chow, with Ziyang Qin, Yuan Liao, and Ayush Khaitan, used the Lean proof assistant to fully formalize Hamilton and Perelman's proof of the Poincaré conjecture, totaling about 4.7 million lines, of which roughly 2.7 million were written in the final two weeks with help from ChatGPT, Claude, and other AI tools. All lines passed Lean's kernel check, with no uses of "sorry".