YAPOAI (Yet Another Post on AI): AI, understanding, and mathematical work

These are some personal reflections on AI, mathematical research, and the current storm they’re in. I have mostly kept to mathematics, where I have direct experience to draw on. My enthusiasm for some of the tools should not be mistaken for a positive assessment of their wider environmental, economic or political consequences. I am extremely concerned about those, and they bear directly on some of the questions discussed below.

---

I use large language models quite a lot in my research. I ask them to look for references, explain unfamiliar mathematics, write code, suggest approaches, find counterexamples, and try to prove things. I don’t see a good reason why the machine should be allowed to prove Lemma 3.2 but forbidden to prove Theorem A. This has been useful. I have also finally started doing something with years of notes of the form “this looks interesting… for later.” “Later” didn’t turn out to be a very effective research plan.

The models still need considerable supervision. My usual response to a promising argument is to give it to two or three other models and ask them to find what is wrong with it, then read it critically myself. Their agreement is not a vote that settles the matter, but their objections often save me time.

I am much less impressed by their mathematical exposition: they can produce paragraphs that look locally reasonable while the text as a whole goes nowhere. Elementary details get several paragraphs, while the key point is hidden in a turn of phrase. I have not seen, in my own use, much evidence of sustained theory-building or of the ability to decide which results should organize a paper.

Even if the models stopped improving tomorrow, they would already have changed how I work. But that doesn’t settle what their place in mathematics should be, and it certainly doesn’t settle whether I approve of the companies developing them.

What are we trying to do?

The things I value most in mathematics are creating concepts, understanding structures, and explaining why something is true. Beauty and the pleasure of figuring things out matter a great deal too. Solving a recognized open problem is not necessarily a priority.

(Of course, this is a description of my tastes, not a formula for distributing the world’s research budget. I am working on pure math, but an applied mathematician may put applications first. The priorities of society do not necessarily coincide mine. Even within pure mathematics, I would not expect everyone to share my ordering.)

A hundred times more theorems would not automatically make my mathematical life a hundred times better. Thurston’s On proof and progress in mathematics (1994!) remains an excellent reference here. His starting question is how mathematicians advance human understanding of mathematics, rather than simply how they prove theorems. We are not inventing a consolation prize for humans now that machines have become inconveniently good at proving things.

There is a related issue about our community. David Bessis argues that proving a difficult theorem has served as a publicly recognizable sign of mathematical achievement, including achievement that actually took place while developing the language in which the theorem could be stated. Tao describes the broader problem in terms of Goodhart’s law, i.e., activities such as solving problems, building theories, training people, developing understanding, are used to support one another, so one could serve as a proxy for the others. AI is starting to unravel the connection between these activities.

I mostly agree, but I would hesitate to reduce all theorem proving to a proxy for other things. Knowing that a statement is true has value, sometimes enormous, independently of whether I personally find the proof illuminating. A long, ugly proof and a short, conceptual one can accomplish different things, and I’d be skeptical of any claim of the existence of a global order relation (for “good” to “bad”) on all proofs that captures all of this.

Suppose an AI settles a question about configuration spaces that has been bothering me for years. I would certainly be interested! But if I still don’t understand what makes the answer true, then I won’t be satisfied. Perhaps the proof uses a construction I don’t understand yet, or it is a huge case-by-case proof that “should” be replaced by a structural argument. This means the work isn’t “done” yet, even though we know the result is true.

Last, a flood of (potentially) correct results is creating an enormous amount of work: finding the useful ones, connecting them, explaining them, turning isolated observations into a theory. That work will not happen simply because the results exist. Somebody has to do it, and we have to give people the time and recognition to do it. I would say, though, that this issue didn’t start with AI, as even five years ago my daily arXiv notification contained way too much math for one person to absorb already.

Checking is still work

I am happy for an AI to suggest the key idea of a proof. I am not happy to put my name on an argument merely because it sounds convincing. Pavel Etingof’s advice to young mathematicians is close to my own practice: use the tools, but keep up with the mathematics, understand what you are using, and be able to explain it. That obligation does not disappear when the output looks polished, and in fact, polishing can make a gap harder to notice!

I am especially worried about the plausible-looking passages where an extra hypothesis slips in, a construction is called natural without the required compatibility being checked, or a theorem is invoked in a setting where it does not apply. In my experience, an AI can produce a great deal of sensible mathematics around one such mistake and finding it requires real expertise. For now, I therefore approach an AI argument with more suspicion than an argument from a colleague whose work I know.

This is empirical, and if reliable evidence eventually shows that particular systems make fewer mistakes than humans on particular tasks, our practices should reflect that. But how would we know that they continue to be reliable if we stopped checking? A system might perform differently after an update, on a different subject, or on the problems selected by a new workflow. Continuing independent audits would serve two purposes: finding errors in individual arguments, and maintaining the evidence on which our trust rests. Yesterday’s reputation is not a lifetime exemption from scrutiny. This, of course, applies to humans as well.

Formal computer-assisted verification can help enormously. However, suppose a proof assistant checks a formal statement: someone must still check that this statement expresses the mathematics being claimed. The Lean documentation is quite explicit about inspecting the axioms on which a theorem depends. A verified proof of the wrong statement does not settle the intended problem…

On the other hand, requiring a human to read every low-level inference would rather miss the point of using a proof assistant. I can imagine understanding the overall mechanism of a proof while delegating hundreds of technical checks to software. What I would need is a clear account of what those checks establish and how the pieces fit together. “I understand the proof” cannot always mean “I have personally repeated every operation.”

There is also a difference between reproducing a discovery and checking the result. I would like research logbooks recording significant prompts, model versions, failed approaches, interventions and checks. A useful record could summarize the important steps rather than burying them in thousands of pages of transcripts. But an inability to replay the exact discovery process should not invalidate an argument that can now be inspected independently. We do not have a reproducible record of every thought that led a human mathematician to a theorem, after all.

Perhaps we need two kinds of paper

Consider a more uncomfortable case. An AI produces a long, formally verified proof. Experts are able to check that the formal statement is the intended one, and that the certificate has the claimed assumptions. Nobody understands the global argument in a satisfying way. Has the problem been solved? I would say yes. Have we obtained everything we wanted from solving it? Probably not.

Our publication system could make room for both answers. One publication could say: here is the result, here is the evidence establishing it, here are its provenance and the checks performed. Another could say: here is a mathematical explanation, here is the mechanism, and here is how it changes our understanding of the surrounding subject. The second might appear much later, with different authors.

There are precedents. Research announcements have long distinguished communicating a result from publishing a full treatment. The ProofForum prototype also proposes recording generation, checking and human verification as separate contributions. I don’t endorse every feature of these arrangements, but there is no reason to regard our current packaging as engraved in stone.

The distinction I have in mind is not simply between a short paper and a long paper. Also, complete certificate should already be available with the announcement. What comes later could be a new explanation rather than missing details. It might introduce a definition that makes the result natural, replace a computation with a geometric argument, or show that several apparently unrelated theorems are instances of the same phenomenon.

We already recognize that a new proof or a conceptual reorganization can be a major contribution. I would like the publication system to accommodate this separation more routinely. Calling work “merely expository,” as I have read a few times, just because someone else obtained the truth value first, would be a strange response from a profession that says it values understanding.

There would have to be safeguards, obviously. An announcement cannot just be a confident assertion, nor a way to reserve an entire research direction. The supporting material must be available for scrutiny, the status of the checks must be clear, and the record must be correctable. A press release does not become a mathematical publication by acquiring the heading “Result announcement.”

This shouldn’t be, moreover, a separate enclosure for AI mathematics. The distinction concerns what a publication contributes, not how its proof was generated. A human proof can be opaque and an AI proof can be illuminating. I expect that, like yesteryear, one article will often still do both jobs perfectly well.

This would not solve the problem of volume, and correctness is not a sufficient reason to request hours of somebody else’s attention. I could not responsibly check, understand and present ten substantial papers a month, and putting them through a proof assistant would not induce automatically mathematical interest. Authors would still have to select, and editors would still have to exercise judgment.

Distinguishing the two purposes would let us acknowledge a result without pretending that the work of understanding it is finished.

Whose theorem is it?

Suppose I type a well-known open problem into a model and it immediately returns a correct, new proof. What have I accomplished?

My first reaction is to compare this with finding an archaeological artefact in my garden by accident. I have found something important, that is worth recording, but it is not evidence that I possess remarkable archaeological insight.

The analogy has limits: the artefact was already in the ground, whereas the model generated the argument. Still, it helps separate finding something from understanding and interpreting it. If I subsequently spend months working out the proof, locating its antecedents, reorganizing it and explaining its significance, that is substantial intellectual work. It does not retroactively make the initial flash of ingenuity mine.

Most of my actual use is nowhere near this one-prompt scenario. Choosing a useful question, supplying the right background, rejecting misleading approaches and deciding what to try next all involve mathematics. There can be substantial human contribution before, during and after the machine’s contribution. We should describe it rather than inventing a percentage of the paper that is supposedly “AI.”

What matters for attribution is that an idea appeared in its output and did not originate with me. Authorship involves more than that. An author must answer questions, correct errors, investigate missing attribution, and take responsibility for the published text. An LLM cannot assume those responsibilities in the way a member of the mathematical community can. I would keep human authorship while being much more explicit about the different contributions behind it.

Martin Hairer’s suggestions on disclosure are sensible: say what the system contributed to the mathematics. An indication that a particular model suggested the construction in Section 4 or found the proof of a lemma tells the reader something. A vague declaration that “AI was used” tells them very little. Citing the model does not settle attribution to the literature, and “The AI suggested it” is no excuse for presenting an old argument as new. I remain responsible for looking for earlier work. I recently came across a paper from four decades ago, containing a result very relevant to my research, that seems to be little known in my area if I’m to believe Google Scholar (it has less than ten citations). Humans certainly miss references too! But models’ ability to produce useful mathematics without identifying its sources makes a deliberate search for antecedents particularly important.

There is a further distinction that will matter for hiring. The value of a mathematical result and what it tells us about its author’s abilities are different questions. The same proof can be equally useful to its readers while having been obtained through very different kinds of work. A committee evaluating a person should care about that difference. Disclosure shouldn’t lead to punishment, but it cannot pretend that provenance conveys no information.

Training a mathematician

The main outcome I expect from a PhD is a mathematician. The thesis is only part of the process by which that person is formed. Minas Karamanis makes this point particularly clearly in an essay about astrophysics: the project is a means of training the scientist, not simply a deliverable to extract from them. Francis Su makes the corresponding case for mathematics education, emphasizing the habits and dispositions developed through doing mathematics.

Suppose a student spends a year finding a good proof, and then somebody gets essentially the same proof from an AI in three minutes. The student has not retroactively wasted a year: they learned mathematics, developed persistence, made mistakes and learned to diagnose them. Those things did not disappear when the other person pressed Enter.

Conversely, a thesis containing excellent results is not enough if the student has learned very little about how to do mathematics. This is why I would ask a beginning PhD student to spend at least some initial months (or years) working without LLMs on the central mathematical tasks. The purpose of an exercise can be the effort required to do it; Etingof makes this distinction explicitly in his advice on exercises and research. There is no contradiction in delegating a calculation in my own research and asking a student to carry out a similar calculation unaided.

I don’t mean that the mature researcher has finished learning and can safely stop thinking. My ability to criticize the output comes from mathematical work I have done myself. I also notice that an AI’s suggestions can anchor my thinking, which is one reason I try to find a couple of approaches before asking it. And most importantly, there are plenty of questions beyond the tools’ capabilities. We need people able to work on those, not just people able to recognize a familiar-looking answer.

“Give students AI-resistant problems” does not strike me as a particularly good solution. Such problems may also well be PhD-student-resistant. It risks organizing education around whatever the current models happen to find difficult, rather than around what the student needs to learn.

The uncomfortable consequence of this thought experiment is that we may have to rely less on the theorems in a young researcher’s CV when assessing their development. We can ask them to explain an argument, change a hypothesis, explore an example, identify what they do not know… this is called a PhD thesis defense. Turning them into a fair system for comparing applicants at scale is much harder and I don’t have a ready-made solution.

Must the problems remain open?

Hugo Duminil-Copin describes open problems as lighthouses: they guide exploration, bring people together, and generate ideas even when nobody solves them. His account of the mathematics that grew out of failed attempts on a percolation conjecture is a strong argument for taking the process seriously. I recognize that experience, but I am not convinced that the right response is to keep the problems unsolved for longer.

An individual may benefit from trying a problem without looking at its solution. It does not follow that the community benefits from nobody having a solution. We already ask students to prove things whose proofs are sitting in books. I can also spend months looking for an explanation of a theorem that is known by someone to be true. The distinction between personal discovery and collective knowledge is not new.

There is an important immediate objection: a known theorem does not organize a research community in quite the same way as an open conjecture. More prosaically, reproducing a known proof does not have the same career value. Telling an anxious doctoral student to enjoy the journey does not solve either problem.

But then we really have to change what we reward: if we claim that understanding is the point, we should make it possible to build a career by producing important new understanding of already established results. This is another reason to separate the first announcement from the later mathematical explanation. Otherwise, we are hypocrites and our advice to students and our hiring decisions will keep pulling in different directions.

Opportunities to struggle and explore are worth preserving, but preserving our collective ignorance is not a goal in itself.

The companies are another matter

My enthusiasm for the tools should not be confused with enthusiasm for the economic arrangements surrounding them.

The Leiden Declaration calls for public infrastructure, independent research laboratories and greater oversight of the AI industry. The article by Commelin, Jamnik, Ochigame, Taelman and Venkatesh puts mathematical intellectual autonomy at the centre of the discussion, and I definitely agree. Tian Lan also argues that mathematicians should use the tools without handing the companies authority over mathematical judgment.

A company selling an AI service and a mathematician trying to understand a structure do not have the same objectives. Their interests can overlap, as an advertised result can be genuinely valuable. But a famous conjecture is useful marketing in a way that a new definition or an improved explanation usually isn’t. I don’t think our subject was particularly well served by concentrating prestige on a handful of famous problems even before companies acquired a commercial interest in doing so.

Funding and other conflicts of interest should be disclosed, and important claims should come with inspectable mathematics and expert scrutiny. These expectations should apply to a company announcing a spectacular result just as they apply to the rest of us. A larger communications budget should not buy a lower standard.

There is a position, argued e.g. by Tasmin Chu, that these political and institutional dangers give us reason not to use LLMs to produce new proofs. I share a lot of the diagnosis: the current situation is a grave danger to democracy itself. But I don’t accept the general conclusion. The fact that useful technology is controlled by companies with objectionable incentives is a reason to contest that control. It is not, by itself, a reason to give up the technology.

This is not an exemption for my own use and I am not without contradictions. Paying for a subscription contributes to the system I am criticizing. And importantly, my confidence in the value of the tools are conditional to the improvement of their economic and ecological costs. The ecological question is not peripheral to this. Training and running increasingly large models consumes substantial amounts of energy and material resources, and “this produces interesting mathematics” is not by itself enough to justify an arbitrary expenditure. The right comparison is not with some imaginary zero-cost human mathematician, but with the other things those resources could have been used for.

I would support public, openly accessible mathematical AI infrastructure. I would also support strong regulation and taxation of the companies. Public ownership is not as an unthinkable option. Giving universities money that must then be spent on proprietary subscriptions is not the same thing as building public capacity. There is a democratic issue here as well. If tools that become essential to scientific work are controlled by a handful of private companies, then decisions about access, acceptable uses, prices, and ultimately some of the directions in which enormous computational resources are deployed are made with remarkably little public control. Open access matters to me partly for this reason: scientific autonomy is not only about whether I personally can afford a subscription.

Expensive scientific equipment is not inherently illegitimate. How resources are allocated, who controls access, and who receives the benefits, are the key points. A hypothetical €10 million computation that solves a famous conjecture could be a mathematical success and a questionable use of resources. The prestige of the problem does not tell us whether that was a good social choice. “The market was willing to pay for it” is not an answer either. Not to say that public funding would not automatically make every such choice wise; it would still need scrutiny and accountability.

Learning from the commons

On training data, I differ from some of the people with whom I otherwise agree. I am happy for models to be trained on my publicly available mathematical papers as I put them put there to contribute to shared knowledge. I would not opt them out merely because the learner is a machine. Gowers raises a similar objection to the Leiden Declaration’s recommendation concerning training consent.

That does not mean that private research conversations should be treated as public material, or that a model’s output is exempt from attribution. My published paper, a collaborator’s unfinished argument and a confidential referee manuscript are three different things. I would ask a collaborator before submitting our unpublished work to a model, even with a promise that it would not be used for training. For refereeing, the journal’s rules and the manuscript’s confidentiality have to be respected.

The distinction I care about is between making knowledge available and allowing control over the resulting capabilities to become privately concentrated. I don’t particularly want a tiny royalty whenever my paper contributes to a model, this would be meaningless or even justifying an unfair system. I want the benefits of technology built using a shared intellectual inheritance to benefit society. We have broader instruments for that than a separate licensing arrangement for every mathematical article.

There is no contradiction in wanting machines to learn from the mathematical commons while objecting to a few companies deciding what everyone can subsequently do with the machinery.

And if AI can do everything?

I would be wary of defending human mathematics by identifying a succession of things machines supposedly cannot do. First proofs, then ideas, then taste, then explanations. I don’t know where their capabilities will stop, and I don’t want my reasons for doing mathematics to depend on the next benchmark result.

Jeremy Avigad argues for a broader view of AI for mathematics than asking neural theorem provers to do our work and then looking for whatever remains for us. The fact that a machine can do something does not tell me whether doing it myself, or with other people, is worthwhile.

When I visit MathOverflow, part of what I want is interaction with mathematicians. I could ask a chatbot directly if I wanted to. A forum full of people forwarding machine answers would not provide the same thing, even if the answers were correct. Communities can reasonably preserve spaces for human exchange without declaring the technology illegitimate everywhere else.

Still, I would be lying if I said that priority and personal discovery mean nothing to me. They matter quite a lot. I don’t know whether I would have chosen the same profession if it consisted entirely of learning and explaining results that machines had already found. There would be a real loss for me in that change, even if much worthwhile activity remained.

I would nevertheless support people doing mathematics together in such a world, just as I support public funding for art. Understanding something, creating something beautiful, and helping others see it are worthwhile human activities. Whether society should fund my present job in precisely its present form is a different question, and I don’t have a good answer.

For now, AI is helping me learn mathematics I would not otherwise have had time to learn, and pursue questions I had left aside. I am glad about that. I still want to understand what I am doing, and I still want there to be people with whom I can discuss it.