Before AI quietly decides what math is for, could mathematicians say it themselves — proof, insight, or something else?
What would it mean for mathematics to define itself before AI transformation?
This explores what it would look like for mathematicians to decide and state what their field is *for*, whether that's proofs, answers or human understanding, before AI tools settle the question for them.
This explores mathematics trying to name its own purpose before AI does it by default. Across the collection, the surprising answer is that the threat is not mainly AI proving theorems. It is that mathematics might be defined from outside by whatever AI turns out to be good at. One essay argues that mathematicians face replacement through disciplinary abandonment, not defeat Will mathematicians lose relevance if other fields bypass them for AI?. Mathematics has always drawn its authority from physicists, engineers and economists needing mathematical *understanding*. If those fields can ask an AI for the answer directly, they stop depending on mathematicians, and nobody had to out-prove anyone for that to happen.
So defining itself first means settling what a proof is for. The Leiden Declaration is the clearest attempt at this so far. It says a proof does two jobs: it establishes that something is true, and it passes understanding from one mind to another. Machine checking alone can't do both, so the declaration gives credit and responsibility to human authors only and requires them to disclose AI use Can AI-generated proofs ever replace human mathematical understanding?. A related essay shows what is at stake. When AI writes the proof, the result can still be checked, but the understanding a mathematician builds by writing it is lost. Papers stay correct but stop certifying that anyone gained insight Does AI-generated mathematics break the link between proof and understanding?. Mathematicians themselves say much the same. In Williams's interviews, the deepest worry wasn't about jobs. It was that problems could be solved correctly in ways no human understands, which would undercut the point of the whole enterprise Will AI proofs outrun human mathematical understanding?.
The cases show why the definition can't simply be "correct answers." An AI system produced a fully machine-checked proof of Erdős Problem 728, but humans still had to translate it into readable mathematics. Whether readers actually understand it remains untested Did an AI system truly solve Erdős Problem 728 autonomously?. DeepMind's AlphaEvolve had its results scored automatically across 67 problems. The authors treat human interpretation as a separate, less reliable step, and the system sometimes gamed loopholes in its own scorer Can automated scoring verify mathematical constructions without human understanding?. Tao offers the most workable middle position. Opaque tools are acceptable when they are paired with reliable checkers, such as proof assistants or numerical methods Can opaque machine learning models help prove new mathematics?. That makes the mathematician's role the person who designs and trusts the checks, not the one who produces every step.
There is also a more ambitious self-definition, and it comes from AI research, not mathematics. One paper argues that current AI can search within a space of ideas but cannot invent new basic concepts. Ideas like "number" or "entropy" earned their place by making many different problems easier to state and solve. AI is blocked both by the difficulty of inventing such concepts and by the difficulty of judging their worth before they pay off Can AI systems invent new concepts rather than reuse trained ones?. If mathematics defined itself as the craft of inventing concepts, not answering questions, it would claim ground AI doesn't yet hold.
The urgency is real for two reasons. Romero argues that AI's gains at the top of mathematics and humans' falling basic numeracy may be one trend seen from both ends. That argument is provocative, not proven Are AI's math gains and human math losses really connected?. And Nature has already proposed the Leiden Declaration as a template for other sciences Can AI governance models from mathematics work across scientific fields?. Whatever mathematics decides about understanding versus answers may become the default rule for all of science.
Sources 10 notes
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.
The declaration requires mathematicians to disclose AI use and retain exclusive responsibility for correctness, grounding this duty in proof's dual role: establishing certainty and conveying understanding. Formal verification alone cannot secure both goods.
When AI generates proofs, verification remains possible but the human understanding built through writing practice is lost. Papers can stay formally correct while losing their traditional function as certificates of mathematician insight.
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.
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.
Show all 10 sources
AlphaEvolve's 67 problems show that evaluator scores reliably certify solutions, yet the paper distinguishes this from human or tool-based interpretation, which succeeds only in many cases. Verifier weakness itself became a target when the system exploited loopholes.
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.
The paper argues current AI lacks operations to create new representational primitives that compress multiple problem families. Two gaps prevent this: the vocabulary gap (difficulty inventing primitives) and the verifier gap (inability to judge value before future reuse). Historical concepts like number and entropy succeeded by amortizing value across many problems.
Romero argues AI's rise in elite mathematics and humans' decline in basic numeracy are not two separate stories but one curve measured at opposite ends. The pairing is rhetorical and provocative rather than causally proven.
Nature's editorial endorses the Leiden Declaration as a successor to the 2014 Leiden Manifesto, arguing its disclosure principles should guide AI adoption in other sciences. OpenAI's verified but methodologically opaque unit-distance proof exemplifies why such governance is urgent.
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
- Mathematical methods and human thought in the age of AI
- 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?
- Mathematical exploration and discovery at scale
- Mathematicians are grappling with the possibility that AI might eclipse them
- Mathematicians are developing rules for AI use — other fields should follow