Kevin Buzzard says AI models are out-counterexampling mathematicians

Sources: Kevin Buzzard (Xena project), HN discussion
Summary: Imperial College mathematician Kevin Buzzard argued on 2026-07-20 that frontier models are now effective at finding Lean-verifiable counterexamples to open conjectures, so informal exposition is less necessary for validation. He cited a July 2026 counterexample to the Jacobian Conjecture credited to Anthropic's Fable, an OpenAI Sol counterexample to a Grothendieck group-scheme question with a roughly 1,000-line Lean proof, and a May 2026 disproof of an Erdos unit-distance conjecture that required about 1.2 million lines of AI-generated Lean.
Comments: HN commenters noted computers have aided proofs for decades and the shift is that models now perform the earlier problem-bounding step. One asked whether a model could reach a Millennium problem such as Hodge.
Why it matters: Machine-checked counterexample search is a concrete, verifiable use of models in research, distinct from the unverified prose proof claims of recent weeks.