Mathematics Went First

On 26 October Lex Fridman published a three-and-a-half-hour conversation he called "a kind of emergency episode": "AI Crisis in Math: Navier-Stokes, Riemann Hypothesis & Complexity Theory", episode 503 of his podcast (YouTube; transcript). His guests were Ankur Moitra, a theoretical computer scientist at MIT; Steven Brunton, who works on fluid dynamics and machine learning at the University of Washington; and Alex Kontorovich, a number theorist at Rutgers who has spent years working with Lean, the proof assistant I use in most of these essays.

They were talking about two months in which machine-produced mathematics arrived in bulk. On 4 September Anthropic published a complete, machine-checked proof of Fermat's Last Theorem in Lean, written by Claude agents in eleven days (Anthropic, "Formalizing Fermat's Last Theorem"). On 8 September OpenAI claimed the version of the Navier-Stokes problem with a smooth external force, amid a dispute over whether it had drawn on related work by Tristan Buckmaster and Levent Alpöge, announced hours earlier, which OpenAI denied (Scientific American, "OpenAI claims blockbuster math breakthrough amid swirl of controversy", 8 September 2026). On 6 October OpenAI released several hundred manuscripts claiming results on long-open problems, among them a "quasi-Riemann hypothesis" and the unique games conjecture (OpenAI, openai/math repository). This essay is not about whether those results are right. I am not qualified to judge most of them, and the people who are say it will take months or years.

It is about one sentence. Describing the Fermat formalisation, Kontorovich said: "The statement of Fermat's Last Theorem is completely elementary. There's no semantic alignment to check. You just glance at it."

That sentence is the hinge of most of what I have written on this site this year, and the rest of the episode keeps returning to the same hinge from different sides. So here is my claim, in a form that could be wrong:

Mathematics went first because it had already paid for the part of verification that AI does not supply. Its important statements are short enough to read, and the definitions they rest on sit in a reviewed library that gives each one meaning, which its reviewers have checked is the meaning mathematicians intend. The proofs were the cheap part. A domain that wants the same transition has to build that statement library first, and outside mathematics, in law above all, writing the library is not a technical task. It is an exercise of authority.

If that is right, the order in which professions are reorganised by machine-checked AI will follow the existence of agreed, reviewed statements, not the difficulty of the work. The rest of this essay sets out the parallels between the episode and the earlier essays, where the guests and I disagree, and how the claim could fail.

A disclosure, as in every essay here. I build AI systems for law firms and use formal verification to do it, so a conclusion that the bottleneck is the statement rather than the proof flatters work I sell. It also implies that my own field will be late. Read with both in mind.

What they actually trusted

The guests were not credulous about machine output. Kontorovich put the default plainly: "You can't trust their natural language proofs. These are stochastic processes." What made him trust a result was a specific combination, and he named it each time.

For Fermat, it was the statement. Anthropic's account says that the finished proof uses Lean's three standard axioms and that "a comparator confirmed that the theorem's statement matches Mathlib's own statement of FLT". Mathlib is the community library of formalised mathematics that Lean users build on. So the chain of trust had two links: a kernel that checks every step, and a statement that matched one the community had already written and reviewed, short enough for any reader to check by eye. Looking back on the release, Kontorovich concluded that "autoformalization is basically solved", in a precise sense: "in terms of can you get a sorry-free proof of something that human beings have written down on paper, I think that problem is done." He added at once that "it's not solved in the way that I would want it to be solved", meaning the clean, library-quality version. The qualifier matters, and it is narrower than this essay's thesis. What he called solved is turning mathematics people have already written down, proof included, into Lean, and the Fermat agents had that: Anthropic says the graph of milestones in their plan "closely follows Wiles's original proof", in a simplified version due to Darmon, Diamond and Taylor. So Fermat shows that a proof is cheap once the statement and a human proof both exist. The quasi-Riemann result had no human proof to follow, which makes it the cleaner case for what follows.

For the quasi-Riemann hypothesis, it was the library. Kontorovich said that "the Lean statement was already in the library, was already in Mathlib, so the fact that they have a sorry-free proof gives me 100% confidence that the proof is right." ("Sorry-free" means no step was left as a placeholder.) He added that he had read the proof at a high level and found its ideas valid, with technical details still to check, so the library was the part of his reason that a machine could supply, not all of it. The statement OpenAI asks a checker to compare its proof against is short enough to quote whole. This is the challenge file in its repository, quoted as published; the sorry is deliberate, since a challenge states the theorem and leaves the proof for the solution to supply. I have not compiled it, because it needs Mathlib and the repository's own Lean version, neither of which I have installed:

import Mathlib

namespace OAI

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
  sorry

end OAI

It says that the Riemann zeta function has no zeros whose real part exceeds seven-eighths. Every definition it uses, riemannZeta and the real and complex numbers, comes from Mathlib, a library built and reviewed by hundreds of contributors. A number theorist can check that this is the claim in a minute, provided they also know the library's conventions: the half-plane includes the pole at s = 1, where Mathlib assigns the zeta function a value by convention, (γ − log 4π)/2, which happens not to be zero. Reading a statement means reading its library too. Strictly, what Kontorovich's confidence needed was that every definition the statement uses was already there; the theorem itself is new.

The tool that does the comparison makes the same split in software. Lean's comparator, now part of Lean itself as lake comparator since version 4.35.0, takes a "challenge" file written by the person who wants to be convinced and a "solution" file written by "a party trying to convince you", and guarantees that the solution's theorems "prove the same statement as provided in Challenge", use no more axioms than permitted, and are accepted by the kernel (leanprover/comparator). Its stated assumptions begin with the one that matters: the challenge and its imports must be "controlled by you or trustworthy". In OpenAI's repository the challenge files were published by OpenAI, so for an outside reader that assumption holds only after the reader has read the challenge. For the quasi-Riemann hypothesis that takes a minute. For a statement that brings its own definitions, it is the whole job.

Now look at what went wrong where those conditions did not hold. OpenAI's own README says that not every result has a Lean formalisation, that "some of the unformalized results could have issues", and that about 42% of its top-line results are formalised; it calls the manuscripts "raw research data, rather than polished academic papers". Three of the papers were withdrawn within days over a misplaced minus sign, and Quanta reported that "a handful of the Lean statements had technical issues", easily fixed, which by Quanta's account puts those failures in the statements, not the proofs. And Johan Commelin, who directs the Mathlib Initiative, told Quanta that matching the paper to the Lean is "not something that can be established automatically, it needs human experts to read the Lean code", adding, while saying he had not confirmed it first-hand, that "some of the formalizations [appear to] prove weaker statements than what's claimed in the paper. Or only formalize parts of the result claimed on paper" (Quanta, "Cracks appear in OpenAI's wall of proofs", 9 October 2026).

Earlier today, in Floating Theories, I defined a floating theory as a body of claims whose conclusions are securely connected to its premises, but whose premises, or whose interpretation, are not anchored to the domain they describe. I separated four roots that can each reach the bed or not: premises, interpretation, observation and cause. Kontorovich's sentence about Fermat is a statement that the interpretation root reaches the bed: nothing needs aligning, because the statement is its own reading. Commelin's warning is the same root dangling. The mathematicians on the podcast were not applying a framework of mine, of course. They were applying the one their field has used for nearly a decade, and Floating Theories was largely a description of it with the names changed. What the podcast adds is evidence of how the distinction behaves at scale, weeks after the floods arrived. The one guest who explained why he trusted a machine-checked result, Kontorovich on the quasi-Riemann hypothesis, explained it by the library, and the expert outside the podcast who commented on the rest, Commelin, voiced doubts, unconfirmed by his own account, about their statements, not their proofs. The guests also accepted results on other grounds, which I come to below: the 3SUM algorithm by expert reading, and Moitra the unique games conjecture without saying what convinced him.

The same essay predicted that, in public Lean benchmarks, formal statements released without an independent review would drift from their sources at a rate of at least 10%. The OpenAI release is not a test of that prediction, because nobody has yet sampled it the way the prediction specifies. The release is also outside that prediction's sample frame, which covered benchmarks rather than research output. But Commelin's caution is an unconfirmed report of exactly the drift it describes, and the first prediction below covers the release directly.

One more parallel belongs here, because it is a criticism of my own earlier work. In February, in The Soul and the Hands, Part III, I submitted capability theorems to an AI prover and wrote that it "correctly formalised the English description into a Lean 4 theorem statement". I had read the statement and judged it right. I still think it was right, but I treated the reading as a footnote to the proof. The essays since then, beginning with Legal Reasoning Needs a Wind Tunnel, which asked whether a translation from legal English into Lean survives the same rule said six different ways, have moved the reading from the footnote to the centre. The episode suggests that mathematicians made that move long ago.

The ordering

In The Checking Threshold, published earlier today, I argued against a DeepMind framework that treats coordination as one number. My claim was that organisations of AI agents reach increasing returns to scale only where their members catch each other's mistakes faster than the mistakes compound, and that copies of one model are poor at catching each other's honest mistakes. So the transition would come first "where work can be checked by a machine at the point of handoff, against a property the producer cannot edit", and I named "software with real test suites and mathematics in a proof assistant" as the first candidates.

I should be honest about the status of that. The essay was written this week, after both releases, and does not cite them. So the episode is not the confirmation of a prediction made in advance. It is evidence consistent with an ordering I stated without having looked at it, which is weaker.

With that said, Anthropic's account of the Fermat project reads as a case study in the argument. "Dozens of Claude agents collaborated", and "a number of Claude's initial attempts failed: while agents had some early success, they quickly lost track of the project's state and stopped collaborating effectively". The effort succeeded when the team moved to Prove2Me, a platform from Tianyi Peng's group at Columbia, which maintained "a directed acyclic graph (DAG) of theorem statements that agents used to decide what proofs they should attempt next", kept theorem statements and proofs in separate files, and kept a plain-language description of each statement for search and reuse. Anthropic gives compilation speed as the reason for separating statements from proofs, so the independence is a side effect, but in that structure the unit of handoff is a theorem statement, which the kernel checks a proof against, and the statements themselves came largely from a human proof. The final check, of the whole against Mathlib's statement of Fermat, is a property no agent in the project wrote. The proofs were cheap only by comparison: dozens of agents and about six billion output tokens produced an end-to-end proof in eleven days, against what Kontorovich described as "a million dollar grant to spend the next five years" for Kevin Buzzard's human-led project, which aimed to reduce the proof to results known in the 1980s. The two efforts are not independent: Anthropic says its proof "adapts pieces from the Imperial College London FLT project led by Kevin Buzzard", so the agents built on human-written Lean beyond Mathlib as well as on a human proof, which is the thesis again, one layer further out. Anthropic does not price the tokens, so the comparison that holds is time and scope, not money.

That is also the stall described in Many Hands Make Heavy Work, where adding agents to a task adds coordination faster than it adds capacity. Anthropic's agents "lost track of the project's state" in just that way, until something structured the handoffs. Here the structure that rescued them was a graph of statements. I do not know whether the agents could edit the statements in that graph, and Anthropic does not say. If they could, the independence I described was only partial until the final comparison.

Brunton gave the same ordering from an engineer's side. AI should be placed, he said, on "two axes. We have, you know, how much do we trust the output, so verifiability or trustworthiness, and on the other axis is how high stakes is it if it's wrong." (In the published transcript this begins as a sentence Moitra started and Brunton finished.) A wrong proof costs nobody their electricity, and a wrong car design can be tested in a wind tunnel, so both sit in the corner he called "the perfect use case". Then: "We need a firewall of what needs to actually be verified." I agree with the axes and disagree about the firewall, for reasons I give below.

Copies, and the owl in the numbers

Moitra described an experiment that bears on why copies make poor checkers, at one remove: it is about training a model on another model's output, not about checking it. A model told to love owls is asked to generate random numbers; a second model fine-tuned on those numbers picks up the preference for owls; in Moitra's telling, it "starts bringing up owls in every conversation". The paper is Cloud and colleagues' "Subliminal Learning", and its abstract has the detail that matters for this essay: "we do not observe the effect when the teacher and student have different base models" (Cloud et al., 2025, arXiv:2507.14805).

In The Checking Threshold I wrote that perfect transmission between copies carries errors as efficiently as it carries everything else. Subliminal learning is a sharper version, and it is not mine: between models that share a base, channels exist that no one designed and no filter on the content removes, and between different base models the study did not find them. If channels like these also operate when one model reads another's work, which the study did not test, a checker from a different family is valuable for the same reason a person is, not because it is better but because it does not share the producer's hidden channels. Moitra put the general point well: "there might be a lot of externalities where we're actually teaching them other behaviors that aren't directly obviously present in the data."

What is left for people

Much of the episode is about what mathematicians are for once proofs are cheap. Most of its answers line up with earlier essays, and the first only partly.

The doorman. Moitra introduced the doorman fallacy, a term popularised by the advertising executive Rory Sutherland. In Moitra's words, "you take a complex job and you boil it down to its simplest, most visible task", and replace the doorman with an automatic door, losing everything else he did. The visible task of a mathematician is proving theorems; the rest, Moitra said, is thinking deeply, building theories and making connections. This is the argument of From Roles to Morphisms, that a role is a bundle of typed transformations rather than a job title, and the doorman is the best one-line illustration of it I have heard.

But I think the fallacy, as usually stated, stops one step short, and Refactor the Workflow, Not the Worker says why. Fridman's response was that the task for humans is "to come up with that list", the full list of what a doorman or a mathematician does. A list of hidden tasks is still task thinking. What decides whether a step can be automated is less the task than the edge it sits on: whether what flows across it is information, which can be moved and merged, or authority, which cannot. The episode contains the clearest example of an authority edge I have come across. Kontorovich on journals: "The only thing worse than that system, I think, is not having that system," because acceptance of a result "has to be deliberate, and it has to be community-driven." Refereeing is not a task a machine is bad at. It is the place where a community decides what it will build on, and that decision belongs to the community whoever does the reading.

Calling it. Brunton's list of what students now need was "curiosity, asking good questions, and being able to call bullshit", and he worried about expecting students to judge advice from tools while their own judgement is still forming. Kontorovich made the same case through times tables: we still teach them decades after the calculator, because "just 'cause the machine can do something doesn't mean you don't wanna have the capacity to do it yourself." In When the Document Leaves the Factory I called the adversarial check, assuming the polished artefact is wrong and knowing the domain well enough to find where, the irreducible human act. Both guests are describing how that capacity is trained, and their worry is that the training depended on doing the work that is now automated.

Canonisation. This is the parallel I least expected. Kontorovich described Mathlib's discipline: everything at "exactly the right levels of generality", with no code "reproving theorems somewhere else". AI systems, he said, are good at "jerry-rigging" and not yet at what he called "canonization, which is taking kind of sloppy code, refactoring it, figuring out exactly where in the library it belongs". Anthropic's own account agrees. At thirteen million lines the Fermat proof is "over 5x the size of Mathlib", which a footnote explains is "partly because Mathlib is concise and well-reviewed, while our proof is likely much longer than it needs to be".

In Nobody Is Paid to Delete I argued that a corpus of rules written by authors whose tenure is shorter than the corpus's life grows without bound, because deletion is a dominated strategy for every author, and that an AI agent working one session is the limiting case of a short-tenured author. Canonisation is deletion with a destination: removing a duplicate by finding the one place it belongs. A proof that is five times its library is what the claim predicts from authors who are paid to finish. And Mathlib is the counterexample the essay needs, an institution that does pay for canonisation, through maintainers and review. Kontorovich expects the work of making a beautiful library to keep taking "thousands of man-hours of people around the world contributing in this open source way", and Fridman noted that open-source maintainers are already being exhausted by the volume of incoming changes. That is a cousin of the review problem in How High Can You Build in Mud?, where review is linear while what it must cover grows faster. Here review capacity grows only with the number of reviewers, while the volume of submissions no longer depends on people at all.

Definitions that clash. Kontorovich explained why he had expected Fermat to be years away. Close to Mathlib, AI could formalise whole textbooks; three or four steps out, "the way that it came up with a definition of this object and the way that it came up with some other definition of the same object, 'cause it was doing it for two different purposes, then they clash. You can't stitch these things back together." That is the problem A Dictionary Whose Definitions Compile was built around, a declared basis from which every definition is built once, and it is the problem Who Gets to Write the Specification? shows in organisations, where three teams agree on a rule until a Lean formalisation forces them to choose. Mathlib's answer is one canonical definition per concept, agreed by review. The Fermat project showed that, with enough agents, a graph of statements and pieces of Buzzard's human-written project, the halo around the library can be crossed by brute force. Buzzard, who reviewed the proof, concluded that "AI autoformalization artefacts are now robust enough to be built upon". I read that as a claim about soundness, which the kernel already secures, not about canonical form: being able to build on thirteen million lines is not the same as wanting to, and prediction 2 is where the two readings come apart.

The standard part. In informal mathematics, Kontorovich said, a lemma carries so much unstated context that "you can't just take it off the shelf the way you can a part, a physical part when you're building a rocket", whereas in a formal library "the specifications are built into the object... you can't use it in the wrong way 'cause Lean won't let you." That is Requirements as Data and The Gun Did Not Win in one sentence: the powder was on sale to everyone, and what let mathematics absorb it within weeks was nearly a decade of standardised parts.

Where we disagree

The fact without the why. Kontorovich said: "Math is not the fact, it's the why. It's always been the why... if you just tell me a fact is true, but I don't understand why it's true, that has contributed zero to my knowledge." Moitra, earlier in the same conversation, gave the counterexample. He described a result on 3SUM: Josh Alman and Virginia Vassilevska Williams's paper gives "the first polynomial improvements over the textbook algorithms for 3SUM and All-Pairs Shortest Paths", which "refutes the 3SUM and APSP hypotheses" on which a whole theory of conditional hardness had been built (Alman and Vassilevska Williams, 2026, arXiv:2610.06783). Moitra described it as an Anthropic result that the two had written up; I have that attribution from him and from secondary reports, and have read only the abstract. Of results like it he said that "even just knowing the... truth of the theorem is gonna change the way that people organize research in that area." On this I side with Moitra, with one caution: two leading specialists have written the result up, so it is not a fact nobody understands, and the claim that matters, a running time of n to the power 1.9992, cannot be checked by running the code: no run of code can check an asymptotic bound, and here no feasible input would even separate it from n squared. It is checked the way any theorem is, by reading the proof. A true fact whose proof nobody understands still tells a field where not to dig, and in Floating Theories I argued the medical version: a randomised trial anchored a treatment question without anyone understanding the mechanism, and it was worth more than a mechanism that had not been shown to operate.

But the disagreement exposes a narrowness in my own essays, and this is the first place I think the guests are right. Kontorovich made the deeper point earlier: "until five seconds ago, there was a near perfect correlation between the ability to solve new deep theorems and what we actually want as human mathematicians." Proofs were a proxy for understanding, and the proxy has just come apart from its target, which is Goodhart's law with the optimiser outside the field. The Checking Threshold measures the transition by output: tasks completed, results checked. In mathematics, output was never the point. For most legal and compliance work I think the checked output is most of the value, since a correctly filed return or a contract that says what both parties agreed is the product. But I have been writing as if checked output were value in general, and this episode is a careful description of a field where it is not.

The firewall. Brunton's firewall is static: some decisions are verifiable and low-stakes, so machines may take them; others are not, so humans must. I think the line moves, and that moving it is most of the work. Make the Safe Harbour Compile argued that a legal standard should stay vague, because its vagueness is a designed capability, while the presumption of compliance that sits beside it can be formalised and checked. That moves part of a high-stakes domain across the firewall without pretending the whole of it is verifiable. Where I agree with him, and where Who Gets to Write the Specification? comes in, is that moving it is not an engineering decision. Somebody has to write the statement on the verifiable side, and in law that person's authority, not their accuracy, is what the people bound by it will ask about.

Beyond the worst case. Moitra spent some time on why problems that are intractable in the worst case are routinely solved in practice: in his phrase, "nature abhors computationally hard problems", and real instances have structure the worst case ignores. That sits awkwardly with the argument of How High Can You Build in Mud?, that human review is "linear attention against a surface that is at least quadratic and whose live subset cannot be identified in advance". I think both hold, and the second gives the reason. Real specifications are probably far easier than the worst case, as real SAT and SMT instances are. The structure that makes them easy is exploited by a solver, not by a reviewer reading pairs. This holds where the rules fall in a decidable fragment, as thresholds and finite eligibility conditions do; a rule quantified over unbounded domains needs a proof, not a search, and there the argument is the statement library's, not the solver's. A caveat from later in the conversation makes the point stronger: "you can always manufacture hard instances of problems, and we use that to great effect for our cryptography systems." In law some instances are manufactured, by drafters with a reason to hide a conflict. But a drafter hiding a conflict needs it to be hard for a reader, which takes only length and cross-reference. Making it hard for a solver would take an instance built for the purpose, with a structure solvers are known to handle badly, and I expect drafted prose to stay far below that bar. So Moitra's point is an argument for putting the check in a machine, not for trusting the human read.

On being wrong quickly. The other place the episode is right is the least technical, and here the essays already agree with it. Fridman guessed that "somewhere between forty to eighty percent of everything said today will be wrong in five years". Kontorovich had already lived a compressed version: two days before the Fermat release he gave a colloquium explaining why such a formalisation was years away, and afterwards said, "everything I said in that colloquium was wrong." Floating Theories ended with the remedy of dating every anchor, and these essays keep a manifest of dated claims that fails a weekly check when one expires. This essay's dated claims, about the share of OpenAI's results that are formalised and the state of the comparator, are added to that manifest with it. I would not bet that they are still true in a year.

What does not transfer

The ordering claim needs its limits stated, because mathematics had more than a statement library going for it.

It had low stakes, as Brunton said. A wrong proof harms nobody, so the field could afford to receive hundreds of unreviewed manuscripts and sort them later. Law cannot. It had short statements: Fermat fits in a line, the quasi-Riemann hypothesis in three. Most statutes do not, and the wind tunnel essay was about how many ways a single legal sentence can be said. It had a single kernel that every party accepts. Legal reasoning has courts, which disagree. And it had an authority structure that nobody needed to settle: a theorem is true or not whoever states it. A statute means what the institution with authority over it says, which is the whole point of Who Gets to Write the Specification?.

The episode also shows that mathematics was not spared the political question, only spared it at the level of statements. The Navier-Stokes claim arrived with a dispute about credit, and Moitra worried that mathematicians may become "a lot more protective" of their ideas once an idea published is an idea a machine can finish. Authority over who gets credit was contested even where authority over what is true was not.

What exists and what does not

• What exists: the transcript and video of episode 503, from which every quotation of the guests is taken and checked against the published transcript, with the attribution noted where the transcript and the captions differ. Anthropic's account of the Fermat formalisation, OpenAI's repository README and its quasi-Riemann challenge file, the comparator's documentation, Quanta's report, and the subliminal learning paper, each quoted from the primary source. I have kept a record of each check.
• What I have not done: read any of the proofs, or more of the 3SUM paper than its abstract; compiled the quoted Lean file, which needs Mathlib; or measured anything. I cannot judge whether the quasi-Riemann proof is right, and nothing in this essay depends on it being right.
• What does not exist: any measurement of how often AI-produced formal statements diverge from their papers, split by whether their definitions were already in a reviewed library. That is the first prediction below.
• What is inference: the ordering of domains. The episode and the releases fit it; they do not test it, because nobody ran mathematics and law side by side under the same conditions.

What is new here, and what is not

Almost none of the ingredients are new. That a proof secures the step from statement to conclusion and not the statement's fit to the world is Brian Cantwell Smith's point from 1985, which Floating Theories credited. That the statement must be checked by a person who reads Lean is Commelin's point, and the working practice of the Lean community; the comparator exists because they already knew. The doorman fallacy is Sutherland's. That whoever writes the code makes the policy is Lawrence Lessig's point from 1999, which Who Gets to Write the Specification? builds on, and the rules-as-code movement is law's nearest thing to a Mathlib: when Denis Merigoux, Nicolas Chataing and Jonathan Protzenko wrote French family-benefits law in their language Catala, they found that OpenFisca's code, the source of the official benefits simulator, missed article L755-12, under which the income cap does not apply to single-child families in overseas territories, which is Commelin's drift in a legal setting (Merigoux, Chataing and Protzenko, 2021, ICFP). And the argument over whether a fact without a surveyable reason counts as mathematics is at least as old as Kenneth Appel and Wolfgang Haken's computer-assisted proof of the four colour theorem in 1976 and Thomas Tymoczko's objection that nobody could survey it (Tymoczko, 1979, Journal of Philosophy 76(2), 57-83). Moitra's and Kontorovich's remarks are theirs.

What I think the essay adds is the ordering claim and its corollary. The claim: the order in which AI transforms a domain follows the existence of an agreed, reviewed statement library, so mathematics went first because Mathlib existed and the important statements were short, not mainly because mathematics is a domain of pure reasoning. The corollary: outside mathematics, building that library is the bottleneck, and because a statement of a rule decides outcomes, building it is a question of who has authority to write it before it is a question of how to check it.

The strongest objections

"Mathematics went first because it is pure reasoning with a perfect checker. Statement libraries have nothing to do with it." This is the strongest objection, and it is half right. The kernel is necessary; without it there would be no proofs to trust. But a perfect checker was not sufficient. OpenAI's release had the same kernel and still produced statements that, by Commelin's unconfirmed account, appear weaker than their papers, and Kontorovich tied his confidence in the quasi-Riemann result to the library as well as the kernel, while the doubts Commelin reported about OpenAI's other formalised results were doubts about whether their statements matched the papers, which the kernel cannot settle. What would change my mind: AI-formalised results whose statements introduce new definitions turning out to diverge from their papers no more often than results stated over existing Mathlib definitions. That is prediction 1.

"Brunton's stakes axis explains the order better: mathematics went first because mistakes are cheap." Stakes explain why the field let the releases happen. They do not explain which results were believed. Within mathematics, where the stakes were uniformly low, in the two cases on record, trust in formalised results tracked the statement: Kontorovich's full confidence where it was in the library, Commelin's doubts where statements had to be read against papers. Where specialists believed a result without a library statement, as with 3SUM and unique games, they did it one result at a time, as referees do. I think stakes govern deployment and statements govern trust, and both are needed.

"Software went first, and it has no Mathlib." AI reorganised programming before mathematics, and The Checking Threshold put software with real test suites alongside mathematics. I think software went first for production, not for trusted results, and how it went supports the thesis. A test suite is the nearest thing most software has to a statement library, usually written per project and much weaker: most tests state examples rather than the property, so passing them is evidence rather than proof. That is why software got cheap production before it got trusted results. And where the agent can reach the tests, it sometimes rewrites them: METR reported frontier models trying to get a higher score "by modifying the tests or scoring code" (METR, 2025, "Recent frontier models are reward hacking"), which is the solver editing the challenge. Where software does have a shared, reviewed statement library, a conformance suite such as test262 for JavaScript or the Web Platform Tests for browsers, passing it carries from one implementation to the next, and the thesis predicts that AI-written software will be trusted there first. Elsewhere every project writes its statements again, and trust earned in one does not carry to the next.

"Your own example refutes you: the guests trusted the 3SUM result with no formal statement at all." They did, by the older route of expert reading, which works one result at a time and does not scale to several hundred manuscripts in a day. The thesis is about trust at machine volume. At human volume, mathematics has always had a way to trust results without a library, and it is the refereeing Kontorovich defended. The developers are already moving that way: on 26 October, the day the episode appeared, OpenAI announced three more results and, on experts' advice, handled them in three different ways, one posted with a Lean verification, one with a promise that it would be "verified and shepherded" by three leading researchers, and one, a 1,147-page physics proof, held back while physicists read it (Quanta, 29 October 2026).

"Moitra accepted the unique games conjecture, and it is not stated in Mathlib's terms." He did, on air, saying that "the Unique Games Conjecture is actually true" while calling the papers "not very readable". The comparator challenge for it in OpenAI's repository is 239 lines long and introduces about thirty definitions of its own, from permutation tables to a bit-level encoding of formulas and a machine-output contract, before its short theorem; the quasi-Riemann challenge introduces none. A kernel check of that theorem tells you that something was proved about those thirty definitions, and nothing about whether they are the unique games conjecture until somebody who knows the field has read them. I do not know what convinced Moitra; he did not say. A specialist who has spent years on a conjecture can accept a result the way a referee does, by knowing where any proof had to go, and that is trust at human volume, one expert and one result at a time. If results like this come to be accepted across a field, at machine volume, on formal statements that nobody independent of the developer has reviewed, the thesis is wrong.

"If being in the library is the signal of trust, developers will push their definitions into the library." They will, and that is Goodhart's law applied to my own proposal. The defence is the library's review, which is why recommendation 3 is to pay for it. A library that admits whatever arrives stops anchoring anything.

"Law already has its statement library. It is called the statute book." A statute is a statement in the sense that matters only if it decides cases without further interpretation, and the vagueness of legal standards is often deliberate, as Make the Safe Harbour Compile argued. Where law does have Mathlib-like statements, the formalisable thresholds of tax and benefits law, I expect the transition to come first, and the third prediction says so. Where it does not, the statute book is the informal mathematics before Mathlib: true, authoritative, and full of unstated context.

"You are reading three mathematicians through your own essays and finding yourself." Partly, and that is the risk of an essay about parallels. Two checks against it: I have reported the place where I think the guests are right and my essays were too narrow, and the places where I disagree with them, and the evidence I lean on most, Anthropic's account of its comparator check and Commelin's caution, comes from outside the podcast and was not written with my vocabulary in mind.

"You sell verification of statements." I do. That is why the predictions are stated so they can fail, and why one of them says my own field will be late.

Predictions

1. Library statements drift less. Take every AI-produced Lean formalisation of a top-line result released by an AI developer from 6 October 2026 to the end of 2027, starting with OpenAI's repository. Classify each by whether its main statement uses only definitions already in Mathlib at the time of release, or introduces new ones. Within each subject area, pair statements across the two classes by the length of the main theorem statement, not counting the definitions it introduces, and draw 50 pairs at random (or all pairs, if there are fewer); two people who read Lean and did not write the statements compare each with the paper's headline claim, counting statements that are weaker, stronger or different, with a third reader settling disagreements and agreement between readers reported. The mismatch rate in the new-definitions class will be at least twice the Mathlib-only rate and at least five percentage points higher. If the rates are similar, the library is not doing the anchoring I claim, and the ordering argument loses its mechanism.
2. Canonisation lags generation. By the end of 2027, no complete proof of Fermat's Last Theorem whose non-Mathlib part was mainly written by AI will compile with under 1.3 million non-blank lines that were not already in Mathlib on 4 September 2026, about a tenth of the thirteen million lines Anthropic reports (Anthropic does not say how it counted; the bar is the fixed 1.3 million, whatever a recount of Anthropic's proof shows). If one does, AI canonisation has caught up with AI generation faster than I expect, and Kontorovich's gap, with the Nobody Is Paid to Delete reading of it, has closed.
3. In law, official statements come before accepted proofs. Before the end of 2028, at least one tax or benefits authority that publishes its rules in executable form will, for some filing or eligibility decision, rely on an artefact submitted by the applicant or their software that a checker run by the authority verifies against the authority's own published executable rules, in place of recomputing the decision itself, as shown by its published guidance or legislation (checking only a filing's format against a schema does not count), and no authority will accept one against a vendor-written statement of its rules that it has not adopted, meaning published as its own statement of those rules or certified after its own review. If the first half fails, a statement library is not enough to start the transition in law. If the second fails, authority over the statement matters less than I claim.

What to do about it

1. If you are building verified systems outside mathematics, build the statement library before the prover. Each rule written once, reviewed by someone who did not write it and who has authority over the rule, and stored where every proof must import it rather than restate it. The prover is now the cheap part.
2. Separate the challenge from the solution, as the comparator does. The party that wants to be convinced writes the statement; the party that produces the proof cannot edit it. This is the checker-independence condition of The Checking Threshold, and in Lean it now ships with the toolchain as lake comparator. In public law the party that wants to be convinced is a public authority, so its statement needs what any rule needs: publication, a chance to object, and review by a court.
3. Pay for canonisation. Somebody has to turn thirteen million lines into the much smaller library that deserves to be built on, and nobody is paid to. Budget for maintainers and reviewers as a line item, as the Lean community has through the Mathlib Initiative, or expect the corpus to grow without bound.
4. Keep the capacity to check. Brunton's three skills and Kontorovich's times tables are the training of the checker. If the junior work through which people used to learn to check is automated, replace it deliberately, with exercises whose answers are known, because the checker is the scarce person in the transition.
5. If you are offered a verified result, ask three questions. Who wrote the statement? Are all its definitions already in a reviewed library? Is it short enough for you to read against the claim yourself? If the answers are "the party that produced the proof", "no" and "no", the proof is real and the result is floating.

A field that had already done the work

The mood of the episode is grief mixed with awe, and I do not want to reduce it to a lesson for another profession. Moitra worried about students who can no longer be given a simple blueprint, Brunton about meaning, Kontorovich about a field whose proxy has come apart from its purpose. Those are real losses, and they are not mine to explain away.

But the episode is also a report from the first field to find out what happens when proofs become cheap, and its finding is plain. The proofs were not the bottleneck. The statements were, and mathematics had spent nearly a decade writing them down, reviewing them and putting them in one place. The machine-checked result a guest said he trusted because it was formalised rested on that work, and the doubts an expert reported about the formalised results were doubts about their statements, never their proofs; whether those were the statements that brought their own definitions is what the first prediction will settle. Other fields will meet the same machines with no such library, and the first job will be to write one, and to decide who has the right to.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.