To Grieve, or Not to Grieve?

Recent advances in AI that can prove deep theorems have produced a sharp split in the mathematics community, which is described through the lens of grieving: denial (groups pledging to keep mathematics “AI-free,” with figures like Peter Scholze vowing not to use AI), anger (public critiques and outraged posts), bargaining (an Advisory Group - including several Fields Medalists - asking frontier labs to stop privately testing on hard math, to release results responsibly, and to fund human engagement), and depression (students and researchers dismayed or contemplating leaving research after AI one-shot solutions). Concrete flashpoints include claims that proprietary models have produced “significant results” and examples where machine-found proofs come with equations or formal Lean proofs but little human-style exposition, prompting complaints that such outputs don’t teach us why.

The piece argues that debates about whether mathematics is primarily about human understanding (Thurston’s position) or aesthetic/artistic achievement and legacy (Hardy’s) are now urgent, because AI may soon both prove and explain results. Examples such as Elkies-Klagsbrun versus newer rank‑30/31 elliptic curves, Wiles-Taylor-Wiles’s conceptual payoff, and the Langlands literature’s reliance on community knowledge are used to show that human “understanding” is subtle and uneven. Formal proof checking in Lean is presented as a refuge - it enforces rigor and gives confidence - and the writer, who identifies as recently diagnosed autistic, favors formalization while warning that appealing to vague notions of human understanding may not survive rapid AI progress.