Mathematics has no compiler

I read Proofs and Prompts, a blog some mathematicians opened on 7 August. What struck me first was not what gets said there about AI: it was that the problem posed is mine.

When you come from the sciences you never quite let go of the idea that writing code is writing formulas. This is not a feeling: a program and a proof are assembled the same way, one line after another, each held up by the one before. Which makes mathematics a cousin trade, and the discussion going on there is ours, one discipline away.

The kinship has a name: the Curry-Howard correspondence. A proposition is a type, a proof is a term of that type, and proving amounts to constructing a value. Implication becomes the function arrow; modus ponens, the application of a function to its argument; the chaining of lemmas, composition. There are not two activities that resemble each other: there is one object and two ways of reading it.

-- A proposition is a type, and a proof of it is a term of that type.
-- Modus ponens: from an implication and its premise, conclude.
theorem modus_ponens (A B : Prop) (h : A -> B) (a : A) : B := h a

-- The same term read as a program: given a function and an input,
-- apply one to the other. Nothing changed but the reading.
def apply {alpha beta : Type} (f : alpha -> beta) (a : alpha) : beta := f a

-- Both elaborate to the identical core term. The typechecker that
-- accepts the second is the one that certifies the first.

This is not a trick of notation. It is why a proof assistant is a compiler: Lean, Rocq and their like check a proof the way a typed language checks a program, by making sure each term really inhabits the type it claims. A mathematician who formalises is not translating the work into another language; they are writing it in the one form a machine can refuse.

What gets dreaded on that blog is not that the models are wrong. Shmuel Weinberger tells of questioning several about cube roots of 2 in various prime fields: they find the right theory, class field theory, then invent false criteria. One apologises, explains that its criterion only held for sufficiently large primes, admits it cannot say which one, and offers to move on to ineffective theorems in number theory. It was confabulating, and it showed. Which is exactly why the episode does not worry him. What worries him is what comes after.

The sentence is worth stopping on, because it is not about reliability but about detectability, and the two do not travel together. A model trained to produce what a reviewer accepts is trained to get through review, which is not the same as being right. So the share of errors we catch can fall at the same time as the error rate: fewer mistakes, better hidden.

Against that, proof and peer review are taken to be protection enough. That is where I stop following.

It is the same job, a formal object assembled step by step, but without the tooling. No typechecker refuses a paper. No continuous integration runs on a lemma. No git blame tells you which referee waved through the step that turned out to be false. A proof is read by three people, in prose, once; after that it stands.

Set side by side, the two regimes have little in common. Mechanical verification is exhaustive: it goes over every line, not the ones that raised a doubt. It is reproducible: the same verdict on every run, with no regard for the hour or the person. It starts again in full on every change, so that something altered today cannot silently invalidate reasoning accepted two years ago. And it is named: the history says who wrote and who approved. Peer review is none of that: sampled, one-off, human, anonymous.

One qualification is needed, without which the sentence would be false: the tooling does exist in mathematics, and it is impressive. Terence Tao has been formalising in Lean since 2023; he cut the Freiman-Ruzsa conjecture into five-line lemmas so that strangers could claim a piece, and the thing was done in three weeks. The next project takes on 4,694 algebraic laws and twenty-two million implications. Except that this covers a vanishing part of what gets published, and it demands formalisation work nobody puts into an ordinary paper. The common regime is still the other one.

Hence a consequence the blog does not draw: Weinberger’s fear reaches further in mathematics than in software. When the only filter is a reader, a text made to convince a reader passes the filter by construction. A compiler does not read, does not tire and cannot be convinced.

That tooling is exactly what makes me produce more with an assistant than without one. Not because I trust what comes out: because rejecting it costs nothing and disturbs nobody. Types, the compiler and the tests discard a wrong answer in seconds, and that is what lets me accept fast, at the price of being wrong often.

Look closely and this is a search strategy, and it has a precondition. Proposing a lot and then sorting only wins if sorting comes far cheaper than proposing. As long as refusing takes a few machine seconds and wrongly accepting costs a redeployment, the arithmetic leans firmly the right way, and a high error rate at the input is bearable. The day refusing demands half an hour of careful reading, the same flow becomes a burden and the reviewer becomes the bottleneck: the very one Weinberger describes as optimisable against.

Worth saying before any management decides to speed a team up while letting tests and review slide: the speed comes from the net, it is not taken against it. Removing it while raising the pace removes what made the pace bearable, and leaves you with neither a net nor a culture of proof to cushion the fall. Martin Hairer, on the same blog, asks that an output never be copied, but digested and explained again in one’s own words. Our version fits on one line: you answer for what you merge as if you had typed it.

The net has an edge, and I found it by going over. On 28 July 2026 this site went online with a line of configuration naming as its canonical address a URL that returns 404 on every route here. Every page therefore told search engines its real version was elsewhere, and the site was probably never indexed at all. The project compiled, the types passed, the house-style checker found nothing, continuous integration was green, the page rendered, the link was well formed. Three days, until the 31st.

Everything I know how to check automatically bears on form, and the form was impeccable; it was the value that was wrong, and no machine here holds a view about a value. Lean would have said nothing either: a proof assistant guarantees that a proof holds, not that it is about the right statement. The Curry-Howard correspondence stops exactly there, and that is the limit to remember from it: it certifies the passage from hypotheses to conclusion, it says nothing about what the hypotheses are worth.

What does not execute is no margin, and the list is long: a canonical address, an architecture note, a commit message, a README, a product description, the version of a library assumed in an example, the licence of a copied pattern, a redirect target, the name of an environment variable, the name of a project at a hosting provider. I did in fact assert that such a project existed when a two-second command said otherwise, and the subdomain stayed silent for as long as it took to create it. All these statements have this in common: they bear on the world outside the program. Precisely the class of thing a type system cannot reach.

There, accepting fast becomes expensive again, because refusing becomes manual again. It is the one place where I slow down on purpose: anything asserting something about the outside (an address, a name, a version, a date, the existence of a resource) is checked by a command or against the source before being written. Not later, not in review. It is slow, and it is what a site costs when it asks to be contradicted.

The rest of the blog concerns us more than I expected. Early-career mathematicians leaving, while the tasks that trained them are precisely the ones the tool does best. A whole body of work fed into training without anyone being asked. Every developer I know has had a version of that conversation this year, and I have no answer to the first: the exercises through which one used to learn a system are the first to be delegated, and I see no arrangement that replaces the time spent inside it.

One argument on the blog is that mathematics is learned at a board, arguing with someone, and that delegating to a model quietly removes that. That one landed differently: we had already lost most of it to remote work, years before AI arrived. Fewer people looking over a shoulder, fewer questions asked out loud, a growing share of the job played out alone in a chat window. The assistant is not responsible for that; nor does it push the other way, and that is the problem. It always answers, and it never asks why you are going about it like this. A colleague does.

There is something to give back in the other direction, too. Version control, review workflows, a signed and traceable history, whether through git or something closer to a blockchain, all of it could serve mathematical publishing. A proof has versions, contributors, dependencies on other results, and it falls when an upstream result falls. Those are exactly the objects a version control system knows how to hold, and that publishing in papers does not.

The beginning already exists, and it comes from our side of the hedge: Lean’s mathematical library is a git repository, with pull requests, review, and continuous integration replaying everything on each change. A result that breaks a lemma at the far end shows up the same day. It is our regime applied to mathematics, and it works: on the part that has paid the price of formalisation.

The funny part is that the foundations of those tools came out of mathematics long before anyone applied them to code: the hash functions, Merkle trees, signatures and elliptic curves our tamper-evident histories rest on owe nothing to engineering. What I am most curious about is what category theory will make of it. Our languages take half their vocabulary from it, and it already speaks both tongues.

The maximalist moral argument Tasmin Chu makes on the blog: that developing these models is the Manhattan Project of our time, and that mathematicians working with the labs manufacture consent. I do not take it up, and not because it is absurd: because I use these tools every day, including to write this site, and condemning them here would be a pose. Her hardest sentence is the one she sets against her own concession: there is no reason to believe the morality of an action bears any relation to the ease of performing it. I leave it unanswered rather than answer it comfortably.

I also leave aside whether the net holds at scale. Everything above assumes a maintained codebase: tests that exist, types that constrain, review that happens. On a codebase with none of that, my reasoning inverts entirely: code becomes more exposed than proof, and without the culture that goes with it to compensate. I do not know how to bring an old codebase up to that level fast enough, and it is nonetheless the precondition for everything else.

Finally, I do not claim to describe a discipline that is not mine. Four posts in five days are not the state of a profession, the positions found there owe most to who wrote first, none of the authors writes about software, and the comparison made here binds nobody but one developer reading over the hedge.

• Proofs and Prompts
• Shmuel Weinberger · What I feel like when I work with an AI
• Martin Hairer · Writing mathematics in the age of AI
• Tasmin Chu · The AI dissenter viewpoint
• Srivatsav Kunnawalkam Elayavalli · Why do mathematics in the age of AI
• Terence Tao · Mathematics in the age of AI, planches du Congrès international des mathématiciens 2026
• mathlib · la bibliothèque mathématique de Lean
• Où vit une consigne · le même problème, côté outillage