Mathematics is the canary

What long-horizon coding agents did to mathematicians, and what RSEs can learn from the incident and from how they reacted

Dr. Kolen Cheung, Research Software Engineer

Research Software & Analytics Group, University of Exeter

September 30th, 2026

Suppose software were like mathematics

Suppose we could verify every step of a program, the way a proof is checked, and get a program that is 100% correct.
This is not how most software is written, and not how it will be.
But take the limit first, then dial back. Mathematicians are already at that limit.
What happened to them, and how they reacted, tells us what the dial back means for us.

The centre of this talk is what happened to mathematics less than a month ago, when OpenAI announced a solution to the Navier–Stokes Millennium Prize Problem. I claim it is a big deal, not only to mathematicians, but also to RSEs.

The approach I take is a thought experiment first: treat software like mathematics. Suppose we can verify every step of a program, the way a mathematical proof is checked, and get a program that is 100% correct. This is not how most software is written. But I want to take this limit first, see what is happening to mathematics there and what the consequences are, and then dial it back to us, because software is not really like mathematics. I think the dialling back implies two things: understanding becomes even more important, and our job becomes minimizing the leaks.

Mathematics is the canary

Mathematics is the canary in a coal mine for all parts of intellectual life. Its claims can be carefully checked and so we are witnessing the disruption in real time. […] Science, law, public policy, and art will all have to find ways to assess what is valuable amidst the abundant output.

— Bryna Kra, Deep theorems were scarce, September 2026

Research software included. See my link post.

Where this talk goes

The limit

Verifiable signals, and Lean: a proof checked by a machine.

The incident

From the IMO to the Jacobian conjecture and Navier–Stokes.

The reaction

What mathematicians say they are after. And a parallel in cybersecurity.

Dialling back

What changes for research software, on two axes.

Then discussion, and a list of questions I don’t have an answer to yet.

The limit

Where agents got good

In May: from autocomplete to agents, and the December 2025 inflection (journal club).
Why they got good where they did: a verifiable signal.
- At training time: reinforcement learning with verifiable rewards (RLVR).
- At test time: an agent in a loop runs the tests, reads the error, and fixes it.
In August: “You never delete human verification. You relocate it somewhere smaller.” (JIT talk)
Today: what is the smallest place it can go? Mathematics has an answer.

We talked about this in the journal club in May: agents got very good at finishing long-horizon tasks roughly at the end of last year. And they became really, really good around April this year, the so-called Mythos moment, when a lot of security bugs were discovered this way.

The key to understanding that is what happens when you put an agent in a loop and give it a verifiable signal. It gets good, in two ways. One is at training time: reinforcement learning with verifiable rewards (RLVR), a buzzword of the last year. You ask the agent to do something, sometimes it gets it right, and the part it got right gives a signal back, which is back-propagated so that it can learn. The other is at run time, which is what happens on my computer: the agent gets signals like a compiler error fed back to it, and it tries to figure out what happened. These two very similar kinds of signals make the agents very, very good.

I ended the JIT talk in August on the line that you never delete human verification, you relocate it somewhere smaller: from assembly, to source, to a spec, to a harness you can audit. So today’s question is what the smallest place is that it can go, and mathematics has an answer.

Lean: proofs as programs

A theorem is a type, and a proof is a program of that type. If the proof compiles, the theorem follows from the axioms.
A small kernel checks every inference. Tactics, automation and the mathlib library produce the terms that it checks.
To a programmer: a type checker for mathematical reasoning.

theorem add_comm' (a b : Nat) : a + b = b + a :=
  Nat.add_comm a b

Software has formal verification too, e.g. seL4, CompCert, and Amazon’s use of TLA+. We will come back to why it stays rare.

Why mathematicians wanted it, before AI

Hales and the Kepler conjecture

Announced 1998, then years waiting for a dozen referees.
Published 2005: the referees believed it but could not check it fully.
Formally verified by the Flyspeck project in 2014.

Scholze and the Liquid Tensor Experiment

I think this may be my most important theorem to date. […] nobody else has dared to look at the details of this […] Better be sure it’s correct…

A challenge to the Lean community in December 2020, completed in 2022.

Nothing to do with advancing AI. Both stories are in Hartnett (2026). Scholze’s challenge is on the Xena blog (Scholze 2020).

Mathematicians wanted formal proving long before AI. Lean itself started in 2013. By then a couple of different kinds of proof had appeared in the community. The more famous one is the four-colour theorem, about colouring maps: it was proved by reducing it to a large number of cases, each of which a computer checks, and that gives you a proof that any map can be coloured with four colours. But a proof like that is very difficult to digest.

The one on the slide is the Kepler conjecture. Hales announced a proof in 1998, which was a big deal, and it used a lot of computer programs. Then, in the peer review process, the mathematics community failed him. Working through another person’s computation is very alien to mathematicians. It is not how they usually write proofs, it is not how they want to think about proofs, and it doesn’t give them more understanding. He thought the referees were looking at the proof, and for years they really weren’t. It was published in 2005, seven years later, with the referees saying they believed it but could not check it fully.

So he went for a formal proof, because he really wanted to know that it was true. If humans don’t want to check it, why don’t we make a computer check it? That project, Flyspeck, succeeded in 2014 (Hales et al. 2017). It is unrelated to Lean (it used HOL Light and Isabelle), but it is one of the motivations for why things like Lean exist.

I didn’t go through the right-hand column on the day, but it is the stunning one. Scholze, a Fields medallist, was not sure of his own proof, because nobody else had dared to look at the details. So in December 2020 he asked the Lean community to formalize it (Scholze 2020), and they finished in July 2022.

The incident

From crutch to certificate

July 2024

AlphaProof + AlphaGeometry 2: IMO silver. Problems manually translated into Lean; up to three days.

July 2025

Gemini Deep Think and an OpenAI model: IMO gold, in natural language, within the 4.5 hours.

July 2026

A counterexample to the Jacobian conjecture, found with Claude Fable 5.

September 2026

OpenAI: Navier–Stokes blowup. ~10,000 agents, 88 h search + 17 h Lean, 165 pages.

In 2024, Lean was what let the model do it at all. By 2026, the proof is found in natural language, and Lean is the certificate at the end.

This is a timeline of AI mathematics, if you want to use that term.

In summer 2024, Google DeepMind released AlphaProof and AlphaGeometry, names that ring a bell from AlphaGo. They reached silver-medal level at the IMO. But it ran for up to three days, where the contestants get two sessions of 4.5 hours. Anyway, it proved that a computer with a certain harness can do very complicated mathematics. (By the way, mathematicians wouldn’t really think of IMO problems as mathematics. They are a bit more like very difficult arithmetic.)

One detail matters here: it was human-assisted, in that people converted the IMO problems into Lean statements first, and then the system proved them in Lean. So Lean was part of the harness that helped the language model think. Two years ago, which is ages ago, the models were very bad at logic and often made mistakes. With Lean guiding them, when they made a mistake in the logic, the compile failure told them.

In 2025, both Google and OpenAI reached IMO gold level, within the real time limit of 4.5 hours, and reasoning in natural language. So they didn’t need that harness anymore.

Then summer 2026. In July, there was a counterexample to the Jacobian conjecture, found with Fable (“A Counterexample to the Jacobian Conjecture” 2026), the best long-horizon agent at the time. And in September, OpenAI announced its solution to the Navier–Stokes Millennium Prize Problem (OpenAI 2026). It took about 10,000 agents and 88 hours of search to find a proof in natural language, and only after that, another 17 hours to convert it into Lean and certify it. It also generated a paper for humans to read, which is 165 pages.

So in 2024, Lean was what let the model do it at all. By 2026, the proof is found in natural language, and Lean is the certificate at the end.

The Jacobian conjecture, in two minutes

A polynomial map F:\mathbb C^n\to\mathbb C^n whose Jacobian \det DF vanishes nowhere is locally invertible everywhere.
Keller (1939) conjectured that it is then invertible, with a polynomial inverse. “Locally everywhere does not imply everywhere” (John D. Cook).
False for n=3 (Alpöge, with Claude Fable 5, July 2026):

\begin{aligned} F(z_1,z_2,z_3) = \big(&(1+z_1 z_2)^3 z_3 + z_2^2 (1+z_1z_2) (4+3z_1z_2), \\ &z_2 + 3 z_1 (1+z_1z_2)^2 z_3 + 3 z_1 z_2^2 (4+3z_1z_2), \\ &2 z_1 - 3 z_1^2 z_2 - z_1^3 z_3\big) \end{aligned}

\det DF=-2, yet F(0,0,-\tfrac14)=F(1,-\tfrac32,\tfrac{13}2)=F(-1,\tfrac32,\tfrac{13}2).

Easy to check, and it looks like a miracle. Tao still wrote a whole post digesting it. The question was asked by Akhil Mathew.

I want to illustrate what these theorems are, and I chose the Jacobian conjecture because it is easier to digest in this setting.

You have a function mapping from n-dimensional space to n-dimensional space, where the space is complex. You can calculate its derivatives, and their determinant is called the Jacobian. Then you can ask whether it is zero or not. If it is not zero, the function is locally invertible. Think of a line in one dimension: if the slope is non-zero everywhere, you probably have a one-to-one function that you can invert. That is the intuition. There is one more requirement, that it must be a polynomial map, like the example here.

The conjecture is that if it is locally invertible everywhere, then it must be globally invertible. It is just a guess. It may not be true, and it turns out that it is not.

The way it was disproved is by a counterexample, and that is what makes it so digestible: the statement is easy to understand, and the counterexample is easy to understand too. It is one line. Here is a function, calculate the determinant, it is -2, which is nowhere zero. But you can find a few different points that give you the same value, so it cannot be globally invertible. Anyone can check this with a computer algebra system in a minute (Cook 2026).

It also gives you a sense of when a conjecture is interesting to mathematicians: it is very simple to grasp, and it stood for almost a century.

But why this map? F has degree 7, so the determinant could have had degree up to 18, and all of its non-constant coefficients happen to vanish. Tao still wrote a whole post explaining the construction geometrically (Tao 2026a). Checking and understanding are different tasks. Also notice who asked the question: Akhil Mathew. Choosing a question worth asking was the human part.

Why a Millennium Prize Problem is a big deal

The Clay Mathematics Institute named seven problems in 2000, with $1 million for each: “to recognize achievement in mathematics of historical magnitude”.
The Riemann hypothesis and P vs NP are on the list. Navier–Stokes is the one that needs the least background to state.
In 26 years, one has been solved: the Poincaré conjecture, by Perelman, who turned the prize down (and the Fields Medal).

OpenAI says it doesn’t intend to claim the prize. Clay’s rules need publication, two years, and general acceptance by the community.

Navier–Stokes, in ninety seconds

\begin{aligned} \partial_tu+(u\cdot\nabla)u&=-\nabla p+\nu\Delta u+f,\\ \nabla\cdot u&=0. \end{aligned}

u the velocity of the fluid, p the pressure, \nu the viscosity, f an external force.
Start from a smooth, nice initial velocity u_0 (and a smooth, nice f). Does the solution stay smooth forever, or can it blow up in finite time?
OpenAI: it can blow up. A collapsing vortex spins up, like water turning faster as it nears a drain.

Spiralling trajectories move inward toward a vertical vortex axis and stretch outward along it; colours distinguish angular rotation rates. — A collapsing vortex: trajectories spiral inward and stretch along the axis. Image: OpenAI.

For the mathematics, see Unpacking the Navier–Stokes blowup. For why I call it an incident, see the series guide.

This one is the big deal. These are the equations, which we know from fluid dynamics. They are just partial differential equations, simple equations with just enough physics to be interesting.

The question is, intuitively: if everything is nice, so the initial velocity of your fluid is smooth, the force you drive it with externally is smooth, and you have viscosity, would the solution always stay nice? What nice means is in my post. Here, just take it as satisfying some good properties, including smoothness.

The prize statement has four forms, A to D. OpenAI proved the C and D forms: when f is non-zero, the solution can run into a singularity. So it is very similar to the last slide, an explicit construction showing that something does not always hold. In this case, that the solution will always be nice. The picture is OpenAI’s illustration of the construction: the speed diverges while the total energy stays bounded.

Four corners, one week

	no force, f=0	with a force, f\neq0
Euler, \nu=0	blowup claimed by OpenAI; a separate candidate from Anandkumar’s group	blowup claimed by Alpöge and Buckmaster
Navier–Stokes, \nu>0	still open (Clay’s A/B)	blowup claimed by OpenAI (Clay’s C/D)

Only the bottom row is a Millennium Prize Problem. Euler is “also open and very important”, but off the list.
The forced approach was already public, in the work of Córdoba and Martínez-Zoroa.

Claims as of 11 September 2026. See the four corners.

I think this table is one of the key things you need in order to understand the incident, meaning how OpenAI affected the mathematics community.

Ask two different questions: is \nu zero, and is f zero? A non-zero external force is called forcing in the community. \nu is the viscosity, a kind of friction in the fluid that slows things down. The \nu=0 case is called Euler. If you find a counterexample in the forced Navier–Stokes case, that is the C or D form. Navier–Stokes without forcing, where the solution is always nice, is the A or B form. It is still open, and it is much harder: if it turns out to be true, you can’t prove it by a counterexample.

What happened is that in the same week, a few different groups of people were solving different corners of this table, and they were essentially forced to announce their proofs in such a hurry that they were not happy with how they released them.

OpenAI solved the unforced Euler corner first. That solution then became part of the prompt for the roughly 10,000 agents: here is the resolution of the Euler case, try to use the idea on the more challenging one.

Alpöge and Buckmaster had been working on forced Euler as a personal collaboration, and rushed their papers out (Buckmaster 2026a), in a form Buckmaster himself calls AI slop (Buckmaster 2026b). Anandkumar’s group (Anandkumar 2026) went public roughly half an hour after circulating the work internally. And the forced approach was already public in the work of Córdoba and Martínez-Zoroa, which is the attribution question that comes up again below.

Is this an AlphaGo moment?

Like AlphaGo

A public demonstration of a capability few expected.
Superhuman persistence and parallelism: 10,000 agents, long calculations nobody would do by hand.

Not like AlphaGo

Go is fully specified, and a match ranks playing strength across the whole game. Mathematics is many kinds of work: a jagged frontier.
Someone still has to check the result.
Missing: an abstraction that makes a problem easy, like Wiles’ modular forms and elliptic curves, or Scholze’s perfectoid spaces.

It doesn’t need to be an AlphaGo moment to disrupt how mathematics trains people, assigns credit, and supports careers.

Some people say this is an AlphaGo moment. Buckmaster, in his statement (Buckmaster 2026b), calls it “a Deep Blue-Kasparov moment” for mathematics, referring to the first time a chess world champion was beaten by a machine. I would say not exactly. There are similarities, but there are two reasons it is not.

First, it is a jagged frontier. Even from just the two proofs we have seen, both are by counterexample. Proofs that something never happens, we haven’t seen that often. And if you need to build a totally new framework in order to gain the insight to prove something, we haven’t seen that happen yet. So it is very good at this kind of thing, and not so good at others.

Second, you still need a human to check it. In chess and in Go it is obvious who wins. There, it is also more difficult to say what the value of the human is. You might say it is part of our culture, but it is hard to say more. In mathematics, and I think in software engineering as well, we can point at it.

This is the other kind of thing we haven’t seen. Fermat’s Last Theorem was conjectured in the 17th century and proved in 1995. The way Andrew Wiles proved it was to establish a correspondence between elliptic curves and modular forms. Once you have that, you can translate the statement to the other side, and over there it takes a few blackboards. But you need this really abstract correspondence. So far we haven’t seen this kind of advance from AI.

And it doesn’t need to be an AlphaGo moment to disrupt how mathematics trains people, assigns credit, and supports careers.

What the kernel doesn’t check

The statement. Does the Lean theorem say Clay’s C/D? Is divergence the classical divergence? Does smooth include t=0? A mistake here gives a verified proof of a different theorem.
The assumptions. No sorry, no custom axiom, no native_decide. #print axioms should list only propext, Classical.choice and Quot.sound.
Junk values. Lean’s functions are total: the integral of a non-integrable function is 0. A bound on the energy can hold when the energy is infinite.

Perhaps a day or two of expert attention, instead of a year of refereeing. Details in the Lean section.

This comes back to the question from earlier: what has the Lean proof not given you, and what do you still need to check?

First, the statement. Remember that in 2024, humans converted the IMO problems into Lean statements, and the computer proved those. So humans were doing the verification that the Lean statement really means what we mean. It is the same for any AI proof in Lean. This is the boundary: you need to confirm that the conversion into a Lean statement really captures what we are saying, so that you are not proving the wrong thing. By the way, there is now a project that collects this kind of Lean proof: Palomar, a registry of Lean-verified mathematics, which Tao calls “the analogue of a preprint server for Lean proofs” (Tao 2026b). It checks mechanically that a proof proves exactly the statements claimed, and uses an LLM to check that the informal description matches them. So even there, the fidelity of the statement is the part that is left to judgement.

Then the assumptions. There is something interesting in Lean called sorry. I would say it is like NotImplementedError in Python: I claim this, and I will do it later. That is how mathematicians write proofs in Lean, ergonomically. They gradually build up the idea, and fill in a sorry here and there. In the case of Scholze’s theorem, the moment it was proved was the moment the last sorry disappeared from the proof.

And there are some other minor things to check, such as junk values, which together guarantee that the proof is really saying what it says.

So on one hand, Lean on its own is not everything. On the other hand, it is a very narrow boundary that you need to check: perhaps a day or two of expert attention, instead of a year of refereeing.

The reaction

An answer is not a solution

De Toffoli and Duede (2026), After Math: OpenAI produced an answer, and an answer is not a solution. “Historically, the two notions have tended to run together.”
Thurston (1994): “We are not trying to meet some abstract production quota of definitions, theorems and proofs. The measure of our success is whether what we do enables people to understand and think more clearly and effectively about mathematics.”
Thurston again (2010): “The product of mathematics is clarity and understanding. Not theorems, by themselves.”
The Clay Institute’s own page for this problem: “Why ask for a proof? Because a proof gives not only certitude, but also understanding.”
Buckmaster (2026b), on his own Lean-verified Euler write-up: it “can only be described as AI slop.”

Mathematicians aren’t mourning their craft. See After Math, translated for software engineers.

Now back to the mathematicians, to see how they reacted. If I summarize this slide, they are saying that getting an answer is not the point. De Toffoli and Duede distinguish an answer from a solution. Others say that they are not after an answer, they are after understanding.

And they said so decades ago, long before AI mathematics. Thurston wrote that mathematics is not about theorems, proofs and lemmas. There was already a trend in mathematics as a profession towards publish or perish, where more volume is better, so a leader in the field had to remind everyone: this is a by-product. Understanding is the most important thing.

Software engineers tend to read the reaction to coding agents as craft versus product: the craft-lovers grieve, and the product people move on. Seen that way, mathematicians look like craft-lovers who are still in the bargaining phase. I think that misreads them. They are saying the product was never the true/false answer. The understanding is the product.

Let’s also try a proof by contradiction. Suppose only the answer matters. What is the value of knowing that the Navier–Stokes equations can blow up? Not knowing it never stopped us from simulating them, and knowing it hasn’t changed a thing about how we solve them.

What the Fields medallists’ declaration upholds

A Severe Misalignment of AI in Mathematics, 11 September 2026:

Understanding: “solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight”
Exposition: rushed announcements leave “no time for a proper writeup, the isolation of new methods and ideas”
Credit: “severe attribution and plagiarism questions”
Students: “The most precious resources of our profession are students and ideas”

And from the essays that followed: journals should “distinguish and credit the roles of discovery, proof, formalization and explanation” (Kra 2026).

We will come back to this list in the discussion: what is our equivalent of each, and do we uphold it?

The Fields medallists’ declaration (Avila et al. 2026) is quite impressive. It started with 25 signatories and it is 27 now. The Fields Medal is very hard to get, and some people call it the Nobel equivalent in mathematics. The joint statement is very short and easy to digest.

The first point is that solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight. That is what mathematics is about, according to them.

Then exposition: you need to teach other people. It has really happened in history that someone came up with a proof they think is correct, and nobody else understands it, so it doesn’t have much value in the community. Mochizuki’s proof of the abc conjecture is the example. It resembles the AI proofs, and in that sense the AI proofs are not the first to give you an answer that nobody can read.

Then credit. Remember the two-by-two table: the forced approach comes from the work of Córdoba and Martínez-Zoroa, as Buckmaster and others have acknowledged. I think failing to give that work enough recognition accounts for much of the dispute.

And students. Being a mathematics student right now is hugely affected. From what I read, many of them are panicking and asking senior people for help.

Not every mathematician agrees

Timothy Gowers didn’t sign, because of the “tool and proxy” sentence:

“there is a spectrum of attitudes in mathematics to the relationship between problem-solving and conceptual understanding” (his Two Cultures of Mathematics, 2000)
On the flood of AI results: it “would also be likely to increase the amount that was properly digested, which seems like a pretty good bargain.”
His worry is elsewhere: “the social structures that currently support this digestion process will be destroyed and not adequately replaced.”

Remember the problem-solving end of that spectrum. See A flood from within the community.

Gowers is another very famous mathematician, and he explains why he didn’t sign (T. Gowers 2026). Gowers and Tao are two prominent mathematicians who have promoted collaboration in mathematics: massive collaboration, more like open source software than a paper with a few co-authors. The two are very alike in that. But Tao signed the declaration, and Gowers didn’t.

The first quote is from 2000 (W. T. Gowers 2000). Even then, he identified two different kinds of motivation. Some mathematicians care more about problem solving: you ask me a problem, I give you a solution. Others emphasize understanding, and something called theory building, which is understanding in a more distilled sense.

His second point is about the flood of AI results. Some of it has already come in the last several months, and there will be more. If a bunch of AI results are released and they all come with understanding, great. But if they only give you an answer, it is still a good bargain. That is his point of view.

What he worries about is something else, which is the social structure of the mathematics community as a whole: how people are rewarded, which is primarily based on proofs, and how students are trained. A student gets an easier problem, works on it for a few months, gets a proof, and gradually gains what is sometimes called mathematical maturity before starting on the hard things. Now think about AI capability. Even if it is a jagged frontier, you can think of it as a certain level, and it wipes out all the easy problems that a third-year graduate student can prove. What do they do now to gain that capability?

So mathematicians are not one group either. I’ll come back to where RSEs sit on his spectrum.

Same capability, two communities

	Cybersecurity	Mathematics
Persistence, parallelism	Mythos Preview chains four vulnerabilities into one browser exploit	10,000 agents over 88 hours
Hard to digest	curl’s security reports arriving 4–5× faster than in 2024	a Lean-verified proof still has to be understood
A rumour is enough	probes about ten minutes after a public fix	OpenAI started its search on a rumour, which was wrong
The rush lands on people	Daniel Stenberg and the curl team	Buckmaster, Anandkumar: unfinished work rushed out

Security answered with coordinated disclosure. My proposal for mathematics: progressive disclosure.

I am still in mathematics, but here a parallel with software engineering starts, in particular with cybersecurity.

What happened at the Mythos moment is that very persistent, hugely parallel AI agents arrived. Persistent means they can discover bugs that nobody else has, just because they keep looking. And they can reason about those bugs and chain them together into a more severe vulnerability (Carlini et al. 2026). In mathematics: 10,000 agents and 88 hours to solve the Navier–Stokes problem.

The second property is that the output is hard to digest. curl, which everyone uses, has four to five times the volume of security reports it had in 2024 (Stenberg 2026), and since the Mythos moment many open source projects have been flooded in the same way. Similarly, a Lean-verified proof is a very impressive, very long thing that is difficult to digest.

The third property is kind of interesting: a rumour is enough. Anil Madhavapeddy opened a public pull request fixing a bug in one of his own open source projects, and within about ten minutes his own website was being probed for it. He then verified that an off-the-shelf model, given the affected code and a hint about where to look, could produce an exploit in under a minute (Madhavapeddy 2026). Just tell them there is a reward somewhere here, and they can find it.

In mathematics, OpenAI heard a rumour in late summer that another company had resolved two Millennium Prize Problems, and it launched a large-scale search of its own (OpenAI 2026). Once the agents had the Euler result, the search was pointed at Navier–Stokes. Only later, in its exchanges with Buckmaster in the first week of September, did it turn out that nobody had proved a Millennium Prize Problem: the rumour was about Alpöge and Buckmaster’s personal collaboration on forced Euler. So a rumour was enough. Somebody else has proved one, so my AI must be able to do it too; tell the agents there is something to prove here, and they prove it.

Lastly, the rush. Daniel Stenberg of curl describes the flood of reports, his wife worrying about his hours, and his concern for his teammates. Over here, Buckmaster and Anandkumar both had a very rushed last week before releasing their work, trying to get it out before OpenAI’s announcement.

Many of us maintain open source, so the left column is closer to home than it looks. In security, a disclosed bug can be exploited, so there is a real deadline. In mathematics there usually isn’t one, so the harm is the rush itself, and that is why I call it an incident.

Dialling back

Four differences

Mathematics is self-contained. We are not. We work with PIs and domain experts, and have less say in where the work goes.
Requirements are rarely as compact as a conjecture. Even the master equations and initial conditions don’t define a program’s behaviour: discretization, approximation and algorithm all have to be specified too.
No watertight abstractions, and no kernel. Formal verification exists for software, but the specification becomes the laborious part, and see point 2.
No shared culture. Mathematicians have standards that reached an equilibrium over centuries, and could react as a community. RSEs don’t, yet.

Two axes

Correctness

In mathematics, it can be made nearly complete: a kernel, and one opening.
We have more leaks and no kernel, so there is more to look at.
The art is to minimize the leaks, so that looking becomes feasible.

Understanding

In mathematics, complete correctness still left no understanding.
We have less correctness assurance, so understanding matters more, not less.
Long-horizon agents write dead programs.

The picture

An AI proof in Lean is like the left: very watertight. Green means you don’t need to check it. Any opening is where you need to inspect: the translation of the statement, sorry, axioms, and so on.

Software written by agents is like the right. There is a famous saying that all abstractions are leaky. That only happens to software, by the way. It doesn’t happen to mathematics, where they are all watertight. And because of that, you have many more holes: you can’t contain a concept in one place, and it appears elsewhere. So there are more things you need to check, and the tests inside are a sample, not a proof.

So our job in designing agentically engineered software is primarily to reduce the number and the surface area of the leaks, so that we can focus our effort on those holes only.

Correctness: shrink where you have to look

Not new. We never read every line of a human PR either: tests, types, CI and small diffs exist to make review feasible.
Find or build an oracle: something independent, compact, and easy to trust.
- Scientific computing: the model equations, manufactured solutions, the observed order of convergence, conservation laws.
- A small pure function reviewed by hand, used to check the fast one.
- A reference implementation: Bun’s 535,000 lines of Zig → Rust in 11 days, against a test suite written in TypeScript. 19 regressions still got through.
- SQLite accepts agentic bug reports with a reproducible test case, and refuses agentic code.
Review the script that generates the diff, rather than the diff.

This is not new. Even with a PR written by a human, you often can’t take a close look at every line, and standard software engineering practices exist to make human review feasible. With agents, they apply the same way, or even more so.

An oracle is my generalization of what I have been arguing for scientific computing: somewhere that correctness can be defined outside the code, compactly, and checked independently. Where one exists, research software sits closer to the mathematics end. SQLite’s policy is the smallest example (Willison 2026): a reproducible test case gives the maintainer something concrete to check, without having to trust the report. Bun is the largest (Sumner 2026): the old program was the specification and the test suite was the guard, and 19 regressions still got through, because a test suite is a sample.

The bottleneck

Goldratt’s theory of constraints (The Goal, 1984): throughput is set by the bottleneck. Speeding up anything else doesn’t help. Amdahl’s law is the special case for parallel computing.
Agents speed up everything except the human check, so the human check is the bottleneck.
The lever we have is its size: design so that the part a human has to look at is small.
Why not just carry on at our own pace? Baumol’s cost disease (Baumol and Bowen, 1966): a string quartet still needs four players and the same 40 minutes, so as everything else gets more productive, it gets relatively more expensive. What only humans do becomes the expensive part, and that is where the pressure to cut lands. Mathematicians and RSEs could become the next artists.

Amdahl’s law is about parallelization, but the core reason is beyond parallelization: what you can’t accelerate becomes the bottleneck. Goldratt said it for factories (Goldratt and Cox 1984).

Some will say this is no big deal, so why do I need to jump on the bandwagon? I think the answer is Baumol’s cost disease (Baumol and Bowen 1966). The bottleneck doesn’t stay a fixed, harmless cost. Everything around it gets cheaper, so the human part becomes the expensive part, and the pressure is either to skip it, which is shipping code nobody has read, or to stop paying the people who do it. The arts survive on subsidy, and on people valuing them for their own sake. Gowers already worries that policy-makers will think mathematicians are no longer needed. This can happen to mathematicians, or to RSEs, if we are not careful. The alternative to paying for the part that can’t speed up is making it smaller, which is the lever above.

Oracles that carry a theory

Bun’s oracle, the old program and its tests, gave correctness and no understanding.
In scientific computing, the oracle is the physics, which is itself a theory, and the researcher already holds it.
So I think scientific computing has an answer on both axes, and product code only on correctness.

See Where do correctness and understanding live in research software? and Can a theory be laid out?

Why understanding gets lost

Not people versus machines as such: the four-colour theorem and Hales’ Kepler proof were monoliths made by people, and Mochizuki’s layers are ones nobody else shares.

This problem, of agents writing something very long, software or a proof, that is indigestible to humans, is not new to software engineers. For the last 18 months or so, people have been saying that it is happening to them: more and more is built by AI, and they are gradually losing their grasp of what is happening.

The picture is an illustration of abstraction. There are two things in it, and they are independent. Solid or dashed is the field: in mathematics all abstractions are watertight, and a lemma an AI proved doesn’t leak either. In software you also have modules and layers, but each of them is a little bit leaky. Layers or one block is how it was built. It is an exaggeration, but what an agent gives you is like the right-hand column: it doesn’t have much structure. It can of course write classes. What it doesn’t build is a theory, which is what I worry about.

A layer is an abstraction when its statement is much smaller than what is inside it, so that you can use it and forget the inside. Why do people build that way? Because we have to. A human can’t hold 165 pages in their head, so we invent the definition and the lemma that let us put things down. An agent with 10,000 parallel attempts doesn’t share that bottleneck, so nothing pushes it to find the abstraction. Henry Cohn calls the result “cryptic, messy, ad hoc, poorly motivated” (Cohn 2026).

If there is one thing I would bring to the journal club, it is Peter Naur’s 1985 paper, Programming as Theory Building (1985). It is the closest thing I know to thinking about programming the way mathematicians think about mathematics: you build a theory, and the theory is in your head. For Naur, if nobody holds the theory of a program, the program is dead.

So one horrible conclusion I arrived at is that long-horizon agents write dead programs. If you ask them to just keep writing, and you don’t come back to check, the program becomes very complex, and in the end nobody holds its theory.

What do RSEs uphold?

Young. The term was coined in 2012 (the Software Sustainability Institute’s Collaborations Workshop). The first RSE conference was in 2016.
Not one thing. Calling us all RSEs is like calling physicists, biologists, chemists and computer scientists all scientists: true, but very different cultures. Even mathematicians have Gowers’ two cultures.
No shared values yet. Some of us are strongly against AI. Some are against involvement with the military (RSECon25). Some are deeply concerned about the environment. Some see our value in problem solving. Some in being part of Digital Research Infrastructure, which includes people.
Without shared values, we can’t react to the flood as one community, the way mathematicians did.

I didn’t get to the value question on the day. Mathematicians could react with such intensity because they are one community that has, more or less, its own standards, which reached an equilibrium long ago. I feel the value of the RSE as a profession is not so well defined.

RSE is quite new. And a research software engineer is not one thing: calling us a single entity is like saying that physicists, biologists, chemists and computer scientists are all scientists. It is true, but they have very different cultures. As Gowers observed, even among mathematicians the two cultures are a big divide.

So what do we uphold? It varies. And I think not having a common culture and shared values is partly why RSEs, and by extension research data scientists and others, can’t be effective in reacting to the flood coming from AI.

Understanding: where our value lies

Mathematics can say what it values from the inside, because it is self-contained. We can’t: our value is defined at the boundary with the researchers.
Kra: deep theorems were a proxy for understanding, and AI made the proxy cheap.
For us, the code is the proxy. If code is what we are valued for, an LLM replaces us.
So what is the product? The theory we build with the researchers: which question they are really asking, what “correct” means to them, which approximation is acceptable.
My proposal, one among many: our value lies in the communication and translation layer. Technical ability still matters, if not for implementing, then for the taste to translate well and correctly.

RSE as translator

Researcher

What is in their head, and what they say.

RSE

Listening and asking: user stories into requirements. And back again: training.

LLM

A lower-level translator: the spec into a program.

Program

Checked against the oracle, where there is one.

Like checking an English theorem against its Lean statement, the human work is at the boundary. Unlike Lean, there is no kernel after it.

RSE work is primarily problem solving: they have a problem, and our expertise is to solve it technically. Part of the value then lies in communication: extracting user stories, and formulating requirements from them. Extracting user stories is communication. They won’t just tell you. The art of listening and asking extracts it from them, much like counselling does. The other direction of communication is training: upskilling them to use what we provide, even though the theory of the program isn’t in their head yet.

That is what I mean by the RSE as a translator. We translate, by communicating with real people, what they say and what is in their heads into concrete, definable requirements for research software. An LLM can then act as a lower-level translation layer, which takes the spec we translated into an actual program.

This is similar to formal proving by agents: a human still needs to make sure of the translation between the mathematical statement in natural language and the formally defined statement in Lean. The difference is that after our boundary there is no kernel.

Born dead

Naur (1985): a program dies when the team holding its theory is dissolved, yet it “may continue to be used for execution in a computer and to produce useful results.”
Cost recovery moves the RSE to the next project. A Julia project: two RSEs designed it, handed it over, and never touched it again. Born dead, without any LLM.
We are paid for the proxy, the code. The product, the theory, leaves with us.
A partial way out: the researcher already holds much of the theory (the physics), and training can move more of it across.

I haven’t solved this. See Born dead.

There are two implications of Naur’s dead program for us. First, we are adopting agentic engineering in our profession, so dead programs are a problem we are going to face. Second, and I think this is even more horrifying, our project structure already makes us deliver dead software.

Think about a Julia library a colleague and I built. One day we went to a whiteboard and drew a diagram, and there was a certain mental picture in our heads. Once the library was delivered, that was gone. The theory is not in the PI’s head. And in Naur’s sense, even documentation is not enough to carry the theory. That is the horrifying bit. If anything, I’ve shown that research software is often born dead even without LLMs.

I don’t have the answer. I think scientific computing might be a little safer in this regard, because what you write in the program is primarily based on scientific theory, so you already have that theory in mind.

Over to you

What mathematicians uphold. Do we?

Mathematicians uphold	Our equivalent? Do we uphold it?
Understanding is the goal (Fields medallists)	communication?
Time for a proper writeup (Fields medallists)	documentation that explains why?
Credit for formalization and explanation (Kra)	credit for tests, documentation, maintenance?
A solution that opens lines of work for others (Cohn)	open source projects? knowledge exchange?
Students and ideas (Fields medallists, Gowers)	handover, training?

Questions I don’t have an answer to yet

Where is the line between research software you can ship unread, and research software you can’t? (research software)
Can a theory be laid out, and can it be rewarded? (theory and reward)
Is “dead” relative to the reader, so that complexity sets the horizon beyond which agents write dead programs?
Under cost recovery, how do we deliver the theory and not just the code?
What is the RSE’s irreplaceable value?

These are the questions I am still working on, and the third one came up in the discussion.

I think whether a theory can be rebuilt is related to complexity. If someone wrote a 100-line program ten years ago and dropped it on me, I could probably rebuild its theory. So the claim that you cannot rebuild a theory must be related to complexity in some way. I am still thinking about it, but it is kind of like a phase transition. We can describe all the physics of the individual atoms in a gas, but we can’t use that to describe the gas as a whole, only because it is so complex. You go through a phase transition, and you need something like the Navier–Stokes equations to describe it in another limit. I think a program is like that too: it becomes so complex that local understanding doesn’t translate into global understanding. Which is the Jacobian conjecture again: you understand it everywhere locally, and you don’t understand the program as a whole.

Discussion

Slides and the posts behind them: blog.kolen.dev