Lean Code, Not Faster Computers, Made AI Proofs Legitimate

An AI system has proven the quasi-Riemann hypothesis, and mathematicians have verified it.

But something odd happened in the gap between the proof and verification — a gap that reveals why this moment feels revolutionary when the actual capability is forty years old. In 1976, Kenneth Appel and Wolfgang Haken proved the Four Color Theorem using a computer to check 1,936 cases that would have taken humans decades.

The mathematical community's response was suspicion so deep that textbooks hedged the result for years. The proof worked and was correct, but it lived in a domain humans could not enter. The barrier was not the computer's reliability but the mathematician's inability to verify the reasoning — to walk through, check. Understand it completely.

What changed is not AI, it is mathematics itself. In the decades after Appel and Haken, the field developed formal proof assistants, Coq, Lean, Isabelle. That translate human reasoning into code a machine can verify line by line. A proof written in Lean is both human-readable and machine-checkable. The infrastructure for computational verification became part of standard mathematical practice.

This latest AI result lands as a revolution because mathematicians can finally do what Appel and Haken's contemporaries could not. They can enter the machine's reasoning, follow it, check it, and own it. The AI did not become more trustworthy. The mathematicians did. They constructed a language in which they could verify machine reasoning the way they verify peer reasoning. By tracing each logical step themselves. Once you have proved something formally in Lean, you can delegate its application to other machines without re-verification, creating a chain of custody for mathematical truth that runs through code. That shifts what human mathematicians optimize for next. They are no longer bottlenecked at verification but at choosing what to prove.

The AI did not become more trustworthy. The mathematicians did.