AI systems are out-counterexampling human mathematicians — with machine-checked proofs

In a July 20, 2026 post, mathematician Kevin Buzzard documents AI models routinely finding counterexamples to open conjectures and formalizing them in the Lean proof assistant — including the resolution of a 60-year-old question of Grothendieck’s and a claimed counterexample to the 87-year-old Jacobian conjecture, announced the same week. Because the Lean files compile, results are mechanically checkable in minutes; the Jacobian claim is independently arithmetic-checked but not yet peer-reviewed.

What it means Generate-then-machine-verify turns AI output from a claim into a checkable artifact — a pattern that generalizes directly to code.