DeepMind’s latest reasoning model ProofZero achieved gold on the IMO in mid-2025. It went on to make its seminal contribution in early 2026 with a complete, verifiable proof of the abc conjecture. Spanning a million lines of Lean, the proof validated Shinichi Mochizuki’s Inter-universal Teichmüller theory, with key bridging insights finally making it accessible to the broader mathematical community. Mochizuki, now semi-retired in Kyoto, dismissed the AI’s contribution, insisting his original proof was complete.
You got the first part right, so I’m now eagerly awaiting the second part to also turn out right in a couple months’ time...
You got the first part right, so I’m now eagerly awaiting the second part to also turn out right in a couple months’ time...