Christian Szegedy and Jeremy Avigad debate what AI means for the future of mathematics

Two essays on what AI is doing to mathematics reached the Hacker News front page within days of each other in early October 2026. The first, dated 3 October, is Christian Szegedy's 'Is Mathematics Over, or Just Graduating?'. The second, published 5 October, is a guest post by Jeremy Avigad on Terence Tao's blog. Both respond to the same shift: according to Szegedy, AI systems have in recent months become capable of solving conjectures nobody had proved before, while Avigad notes that results which a year earlier would have made respectable publications can now be generated with AI help.

Szegedy: the field is graduating

Szegedy builds the essay on an extended analogy. Mathematicians are explorers in an unmapped wilderness; prestige comes from climbing hard rocks — conjectures — and the climbs matter largely because they forge and test new climbing tools. Applications are mineral deposits that fund expeditions, and theory-building is mapping. AI systems are airplanes: Wright-brothers crude, expensive and short-range, but improving quickly, and lately able to land on rocks that human explorers were still climbing.

The explorers in his story object that the flagged rocks were not very interesting, that some were nearly climbed already, and that planes cannot reach the real mountains. Szegedy calls this a 'static-thinking fallacy' — mistaking today's flight range for a permanent limit. His forecast is that climbing rocks to hone climbing tools loses its point once anyone can charter a plane to any summit, and that cheap flight eventually brings satellites: systematic surveying of the whole terrain for extractable resources. Mathematicians will find that industrial phase ugly, he concedes, but his title gives the verdict — the field is graduating, not ending.

Avigad: the discipline's core holds

Avigad writes from the tooling side of the debate. He came to the topic at a meeting of startups supported by Convergent Research, the organization that oversees the Lean FRO, the nonprofit developing the Lean theorem prover. In his read, mathematicians' public reactions on blogs like Tao's and Proofs and Prompts have been largely positive even as daily workflows face upheaval. What has survived every historical transformation, he argues, is mathematics as a culture of rigorous reasoning and communication; the open question is how to pursue mathematical understanding once routine problem-solving is delegated.

He offers three general answers. The first is to solve harder problems. Foundation models have absorbed the entire literature and never tire, which explains why the AI-generated solutions seen so far share a character: they are problems answerable by assembling techniques that already exist, a reading Avigad credits to Matthew Ballard. Reinforcement learning grades each step only by whether the final trajectory succeeds, he notes, which breeds exceptional cleverness while potentially missing creativity and higher-level strategy.

The second is to think bigger thoughts. His example is Riemann's habilitation lecture — Gauss picked, from three topics Riemann had proposed, the one he was least prepared for — which separated a space's metric properties from its topological ones and introduced the idea of a manifold, work that later became foundational to general relativity and now informs fields from robotics to medical imaging. Crediting Ballard again, Avigad observes that no reinforcement-learning setup could have scored Riemann's choices, because the payoff was diffuse and decades away. The same applies to Galois, Poincaré and Grothendieck. And an AI spinning out theorems that only other AIs find interesting, he argues, is of no value to humans by definition: people remain the arbiters of what matters in mathematics.

Where the two essays diverge

Both authors reject the claim that mathematics is finished, but they locate its value differently. For Szegedy, the field's traditional currency — solving problems to refine one's tools — is about to be devalued, and the discipline's future looks at least partly industrial. For Avigad, the things machines currently grade poorly, such as choosing problems, judging significance and making conceptual leaps with long payoffs, become more important rather than less.

What it means for research tooling

The practical stakes show up in infrastructure. Avigad's vantage point is the Lean FRO, and his argument implies that formal proof assistants become the natural interface between machine-generated mathematics and human-verified knowledge. Szegedy's essay closes the loop from the other direction: his explorers ask the aviation companies to hand over planes so they can test them and find uses, while the companies keep flying over the mathematical terrain to improve their models — the role hard problems once played for the explorers' own hand-made tools.

Why it matters

This debate has consequences well beyond opinion pages. If Avigad is right, the scarce skills shift toward problem selection, formalization and taste, and systems like Lean become the default working environment for mathematicians. If Szegedy is right, the structures built on human problem-solving — prestige from hard climbs, publication norms, what a proof is even for — get repriced within a few years. Graduate training, hiring, funding and the design of proof assistants all depend on which view prevails. Read together, the two essays are an early map of that decision.