OpenAI claims that its GPT-5.6 Sol Ultra model, orchestrating 64 sub-agents, produced a proof for the cyclic double cover conjecture — a problem that had stumped mathematicians for about 50 years — in less than an hour.
https://twitter.com/__eknight__/status/2075643450196971805?s=46
OpenAI has released the full prompt and proof, along with an open-source Lean formalization. The code has passed Lean's kernel verification.