tl;dr: In mid-2026, AI tools (ChatGPT's Sol, Claude's Fable, and startups like Logos and Logical Intelligence) produced and formalized in Lean multiple counterexamples to long-standing math problems, including Erdős' Unit Distance conjecture, a 60-year-old Grothendieck question on finite group schemes, and the 100-year-old Jacobian Conjecture. The author, a Lean advocate, argues large AI-generated math developments are now inevitable and that any PhD student not paying for these tools is making a mistake. The remaining challenge is for humans to extract mathematical insight from these machine-discovered counterexamples.