CMU's Jeremy Avigad Says AI Math Is Bigger Than Theorem Provers

Neural theorem provers keep grabbing the headlines. OpenAI announces solutions to open problems, working mathematicians paste conjectures into ChatGPT and Claude, and every few weeks another model claims a fresh olympiad medal. In a new essay, Carnegie Mellon logician Jeremy Avigad argues that this narrow framing does a disservice to the field, and that the real story of AI in mathematics is much bigger, and much more interesting, than a leaderboard of proof-generating models.

The essay, What is mathematics now, and what should it be?, is a short perspective piece from someone with unusual standing to write it. Avigad is a professor of philosophy and mathematical sciences at CMU, a longtime contributor to the Lean proof assistant, and directs ICARM, an NSF-funded institute whose mission is to advance AI methods for mathematical discovery and collaboration. The title nods to Richard Dedekind's 1888 essay on the nature of number, and the intent is similar: to ask what the discipline is turning into, and what it should be.

The mood in the room

The essay opens on a scene that will feel familiar to anyone who has attended a recent formal-math workshop. Kyu-Hwan Lee, a leading practitioner of AI for mathematics, closed a recent workshop by describing, in personal terms, the emotional challenges of adapting to the new workflows and the changes to the subject he had fallen in love with as a student. For many in the audience, the sense of foreboding was visceral.

That mood has been amplified by a media narrative that AI is coming for the mathematicians. OpenAI has announced AI-generated solutions to longstanding open problems, and many researchers now routinely call on systems like ChatGPT and Claude to help them prove theorems. Students and early-career researchers face particularly uncertain prospects. Avigad's response is to reframe the question entirely.