tl;dr: In a speculative near-future account (dated 2026), mathematician Kevin Buzzard describes how AI tools like ChatGPT's "Sol" and Claude's "Fable" have rapidly generated counterexamples to major open problems—including Erdős' Unit Distance conjecture, a 60-year-old Grothendieck question on finite group schemes, and the century-old Jacobian Conjecture—with proofs formalized in Lean and verified against mathlib. Buzzard argues that AI-generated mathematical developments are now inevitable, that formalization makes verification trivial, and that any PhD student not paying for access to these tools is making a mistake.