OpenAI's Commercial Model 'GPT-5.6 Sol Ultra' Generates Proof for 50-Year Mathematical Conundrum

OpenAI has announced that its commercial AI model, GPT-5.6 Sol Ultra, generated a proof for a mathematical problem that has remained unsolved for over 50 years. While independent verification by the mathematics community is still pending, the achievement marks a significant milestone by extending advanced research capabilities previously reserved for internal models to a commercial platform. Edan Knight, an OpenAI researcher, revealed that the model executed parallel reasoning across 64 sub-agents over approximately one hour to produce the completed proof. OpenAI also published the proof itself, the prompt used, and formalized code in the Lean 4 theorem prover on GitHub.