Now that AI can crank out proofs fast, what's actually left for human mathematicians to do?
What should mathematicians prioritize when machines can solve problems faster?
This explores what mathematicians should spend their time and attention on now that AI systems can produce proofs, counterexamples and solutions faster than people can. It's about where human effort still matters, not whether AI can do math.
This explores what's left for mathematicians to prioritize once machines can produce answers quickly. The short version from the corpus: speed was never what mathematics was for. The scarce thing now is understanding. In Williams's interviews with more than 20 mathematicians, most are optimistic about AI as a near-term tool. Their deeper worry is that problems will get solved correctly in ways no human actually understands, which undercuts what they see as the field's purpose: building shared understanding Will AI proofs outrun human mathematical understanding?.
That worry is already showing up in practice. Erdős problems became a popular AI test bed because they're accessible and range widely in difficulty. Reports from that work treat 'the proof is formally checked' and 'a human understands the proof' as two separate outcomes, and the second keeps lagging behind Why did Erdős problems become a popular AI testing ground?. The Erdős Problem 728 case shows both halves. An AI system produced a Lean proof that a machine checked, so its correctness isn't in doubt. Researchers then had to translate it into ordinary mathematical writing, and whether readers can actually follow it hasn't been tested Did an AI system truly solve Erdős Problem 728 autonomously?. One clear priority follows from this: turning verified-but-opaque results into explanations people can understand. That job is becoming more central, not less.
A second priority is building and choosing the checks. Tao argues that it matters less that a machine-learning tool is a black box, as long as its output goes through a reliable validator such as a proof assistant or a rigorous numerical argument. In his Boussinesq blowup example, a neural network suggested candidate solutions, and humans then confirmed them with perturbation arguments Can opaque machine learning models help prove new mathematics?. Alpöge's counterexample to the century-old Jacobian conjecture points the same way. The AI's contribution was searching a huge space of polynomials, not building a proof Can AI search find what human proof cannot?. Together these suggest a division of labor: machines generate and search, while mathematicians decide what's worth searching for, design the checks, and explain why a result is true.
The less obvious point is that the biggest risk to mathematicians may not be AI proving theorems. One essay argues that mathematics gets much of its authority from other fields, like physics, engineering and economics, needing mathematical *understanding*. If those fields start asking AI for answers directly, mathematics could lose its institutional standing without ever being 'beaten' at proofs Will mathematicians lose relevance if other fields bypass them for AI?. If that's right, a key priority is outward-facing: showing other disciplines why understanding a result, not just having it, is worth paying for.
One caveat: this part of the corpus is mostly interviews, essays and case reports, not measured studies. The case for 'prioritize understanding, verification and explanation' is consistent across sources, but it's argued rather than proven. The essay itself grounds its replacement risk in historical analogy, not data.
Sources 6 notes
Williams's interviews with over 20 Philadelphia mathematicians reveal near-term optimism about AI as a tool, but widespread anxiety that correctly solved problems could exceed human comprehension, threatening mathematics' actual purpose: enabling shared understanding.
Erdős problems became an AI test bed because they span accessible mathematical domains with varying difficulty. However, formal logical certification and human comprehension are reported as separate outcomes, with comprehension lagging behind automated verification.
An AI system generated a formal Lean proof of a logarithmic-gap factorial divisibility result, which researchers then made accessible through informal writeup. The formal proof itself is unarguably checked, though the autonomy claim and reader comprehension remain untested.
Tao argues ML tools' opacity matters less than pairing them with reliable validators like proof assistants or numerical methods. He cites finite-time blowup for Boussinesq equations, where a neural network suggested solutions later verified through perturbation arguments.
Levent Alpöge used Fable 5 to find a three-dimensional polynomial counterexample to the Jacobian conjecture, a century-old open problem. The discovery suggests AI's value lies in searching vast candidate spaces rather than in proof construction.
Show all 6 sources
The essay argues mathematics's authority rests on other fields needing mathematical understanding, not just answers. If those fields turn to AI for direct solutions instead, mathematics loses legitimacy and institutional dependence—a shift grounded in historical analogy rather than measured evidence.
Papers this line draws on 8
The research behind the notes this line reads — ranked by how closely each paper relates.
- The crisis of AI-generated mathematics
- From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
- Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free
- What is mathematics now, and what should it be?
- Machine-Assisted Proof
- Remarks on the disproof of the unit distance conjecture
- Mathematical exploration and discovery at scale
- Mathematical methods and human thought in the age of AI