According to Perceive Beating monitoring, OpenAI stated that GPT-5.6 Sol Ultra, utilizing 64 sub-agents, took less than 1 hour to provide a proof for the "Cyclic Double-Covering Conjecture" proposed around 50 years ago.
OpenAI has publicly released the full prompt and proof text, and has open-sourced a Lean formalization. The relevant code has passed Lean kernel verification. However, this is still a result released by OpenAI. The mathematical community has not yet completed an independent review, so for now, it can only be said that the proof has been provided, not outright claimed as "formally resolved".
