BC-Math_and_AI_2026_v3

Fundamental Mathematics in the Age of AI

The Residue, the Journey, and the Ecology

Benjamin COLLAS

Research Institute for Mathematical Sciences, Kyoto University, Kyoto 606-8502, Japan

bcollas@kurims.kyoto-u.ac.jp · 12th October 2026

Abstract. Large language models have begun refuting long-standing conjectures and, for a few thousand dollars of tokens, solving long-open problems (OpenAI, August 2026). The introspection this has prompted about the future of mathematical discovery is now well under way, and the anxiety accompanying it legitimate - but both, we claim, are attached to the wrong loss.

What machines now produce is the countable part of mathematics - theorems, proofs, refutations - which was always the residue of the work, and not its product. The distinction is old, and not originally economic: a result can be taken in its finished essence, or in the operations that engendered it. The product is human understanding: not a stock of results but a collective, hard-won way of deciphering the world and acting upon it [A]. The two are arcs of a single loop: understanding tells us where to look; looking produces the residue; and taking it up again, one journey at a time, is what rebuilds the shared understanding. Machines are strong on the countable arc, absent from the one that feeds it. The peril is to leave the loop open. AI did not create the confusion between residue and product; it has called a bluff long on the books, driving the cost of the residue towards zero and making the scarce thing visible at last.

A new instrument makes a new way of working before it makes a new result. The pressing questions are therefore institutional: who can check an announced result, whoever announces it; what the work and the training become for the next generation of researchers; and whether the one thing that cannot be mass-produced - the journey that nourishes a shared understanding - continues to be funded. Mathematics, we argue, is uniquely placed among the sciences on the first - a proof answers to no one's permission - and uniquely exposed on the other two: teaching cannot go on as before, and no collective position yet exists; and the journey has never had a price our institutions knew how to pay. The decision is ours.

MSC (2020): 01A80 (Primary) 68T01, 68V20, 00A35 (Secondary)

Forewords. These notes set down a reflection of some three years' standing. Their writing was occasioned by a conversation with Parmy Olson (Bloomberg) at the end of July 2026, and occupied the 27th and the 31st; they can be read as a companion paper to [Ols26]. The OpenAI announcement of 1 August arrived as the first version was being finished, and, to my surprise, fitted the argument without altering it. The release of some 370 notes in October, and the two announcements that accompanied it, did the same at a larger scale; the record of that episode, and what it prices, is set down in the Addendum at the end of these pages, and in the in-text footnotes marked ' A '. They draw on personal experience as a researcher, and on exchanges with mathematical communities, private companies, and representatives of governing agencies.

Reference to economic principles should not be read as a claim of expertise, but as an attempt to reach across to those who have it. Political economy and access are not the frame of this essay, though it meets them where its argument does: openness and verification (§ 2.1), who can appropriate what and who provides it (§ 1.3.3), dependency and sovereignty (§ 2.3), entry cost (Coda). The choice is deliberate - each would demand another register, and a competence this text does not claim.

One question is declined outright: what machine intelligence is. This essay does not ask whether a machine understands; it asks whether the loop is closed, and by whom - understanding being, as Part 3 argues, not a property anything possesses but a passage someone has to make again (§ 3.4).

Why a working mathematician should write this at all, rather than get back to work? The seventh recommendation of the Leiden Declaration makes it a duty: mathematicians 'have a responsibility to support serious science journalism and to engage in public discourse to explain and contextualize artificial intelligence-assisted methods and results' [Por+26]. The questions addressed in this note will be settled by whoever turns up to discuss them.

Contents

Acknowledgements. The author thanks Parmy Olson, whose questions occasioned these notes; Julien Cornebise, whose good-humoured and productive disagreement with an earlier version sharpened the arguments that follow; Rodrigo Ochigame for warm exchanges on AI, Lean, and understanding in May 2026; Mochizuki Shinichi for regular exchanges on how the Math-AI frontier could be shaped; Pierre Dèbes for comments on a previous version of these notes. He also thanks Patrick Shafto (expMath) for checking the passages describing his work, and is grateful to Ariane Mézard, Olivier Wittenberg and Johan Commelin for comments on Version 1 of the manuscript, and the latter for bringing [Ost10] to his attention. Thanks also to colleagues in several countries, within the 'Arithmetic and Homotopic Galois Theory' project and beyond, for many conversations on the future of scientific discovery.

[. . . ] le résultat n'est plus considéré dans son essence si pure soit-elle devenue, mais dans la simple position d'un résultat qui résulte, par suite indication des modes qui l'ont engendré.

- J. Cavaillès, Sur la logique et la théorie de la science [Cav47] 1

1 The economy of the residue

Three claims, in order: that a conservative field is moving faster than it has in generations, and on tools it does not own; that what machines now produce is a real but narrow part of mathematics, and was always the residue of the work rather than its product; and that the economics of the field had already mistaken the one for the other, long before any model was trained.

1.1 A conservative field, moving fast

Thurston · human understanding · Leiden Declaration · ICM 2026 · means of production

Academia - and fundamental mathematics in particular - was built as a place for producing sound knowledge in the service of human understanding 2 : not a stock of results, but a way of deciphering the world and of acting upon it. This is the position on Mathematics of Thurston (Fields Medal 1982): he opens by refusing the obvious question - not 'how do mathematicians prove theorems?', but 'how do mathematicians advance human understanding of mathematics?' (§ 1) - and closes where this essay starts:

[The proposed division of roles into 'speculation' and 'proving'] only perpetuates the myth that our progress is measured in units of standard theorems deduced. This is a bit like the fallacy of the person who makes a printout of the first 10,000 primes. What we are producing is human understanding. We have many different ways to understand and many different processes that contribute to our understanding. - W. Thurston [Thu94, § 5]

The intangibility of the product, or rather its uncountability, makes us, researchers in mathematics, conservative in adopting new tools and new ways of working - no instrument can quickly prove that it helped. It is therefore worth registering how fast the field is currently moving.

The most valuable tool of a researcher in fundamental mathematics is their voice, so the explosion of discussion is itself the measure. Over the past two years researchers have engaged strongly with AI tools:

• In practice: writing, investigating hypotheses, producing examples, paving the field - and working groups forming inside academia for the purpose 3.

• In print: the Bulletin of the AMS gave AI and mathematics two special issues in 2024 [AIM24], and individual reflections have followed - Akshay Venkatesh (Fields Medal 2018) - see [Ven24];

• In community: the Leiden Declaration [Por+26] was drawn up in under a year, and five mathematicians have set out a joint position in the Notices [Com+26];

• In public: the ICM 2026 programme includes a public lecture by Terence Tao (Fields Medal 2006), Mathematics in the Age of AI, see [Tao26];

• In funding: establishment of dedicated funding structures such as DARPA's expMath [Sha25], which explicitly aims at accelerating progress in pure mathematics 4 - and with private capital, in new structures that hire researchers and publishing at pace [Axi26].

A field that changes on the scale of two generations has reorganised its conversation in a semester.

Absorbing new modes of producing knowledge is, in one sense, ordinary work for researchers in mathematics: we did it with computers in the 1990s (§ 3.2.3), and we are doing it with mass collaboration and formalisation since circa 2020. What is not ordinary this time is that the means of production belong to someone else.

1.2 What is being measured

Counterexample search · choice of definitions · ten problems for $2,000 · Goodhart's law · what a benchmark measures

Mathematics is often presented as the ideal measure of AI progress: a proof is right or wrong, where prose is a matter of taste. The measurement is real, but it is worth asking what it measures.

1.2.1 Counterexamples, and the constructive half. Machines have so far produced results of two kinds: counterexamples to standing conjectures, and - more recently, and beyond refutation - solutions to open problems (§ 1.2.2). We take them in turn.

The first kind is counterexample search - killing conjectures, most recently, and among many, the Jacobian conjecture, by Levent Alpöge on July 20, 2026 [FBG26]. This is real, and we do not minimise it: counterexample search is the region of mathematics most amenable to machine methods. It is also the least representative of a mathematician's work, and it already illustrates, structurally, the missing interface between AI companies and academia (§ 3.1).

Disproving a conjecture is like pruning a branch that grew in the wrong direction. It does not tell us in which direction to look; it is not an end result. A counterexample, like any result, is worth the horizon it opens.

The other half of the work - the constructive half - is deciding which definitions are worth making and which objects deserve names. That half is what makes a field rather than a pile of results: a theorem is only as good as the notions it is stated in. As of today, no system yet performs that choosing 5. Pruning accelerates a field only if someone is still choosing which branches were worth growing 6.

1.2.2 What $2,000 really buys. The second kind goes further. OpenAI has recently reported solutions to what they present as ten long-open problems, obtained for roughly $2,000 of tokens [Ope26] 7, and - the part worth registering - published them in good order: manuscripts prepared with human help, arguments shipped with a Lean certificate, and, following a certain interpretation of the Leiden Declaration [Por+26], an explicit refusal to claim human authorship. The same announcement concedes the limit of operating apart from academia: these questions 'cannot be answered by a technology company alone.' 8

Good order, however, is not yet good practice 9. The manuscript - a narrative of the discovery - names no one: no co-author to write to, none of the integrators and writers behind the 'human help'. The letter of the standard is met while its point - a human interface on which the field can build - is left empty; we return to this open loop in § 3.1. 10

It is worth being exact about what the price tag measures.

What $2,000 buys is not a theorem; it is evidence of capability at the tasks the benchmark selected and that evidence holds only for as long as the community that certifies it still functions.

Even that evidence is softer than it looks. Much of what a corpus contains has never been noticed - the connections standing to be realised in a literature nobody can read, what Bessis calls the 'overhang' [Bes26] - and a large overhang certainly weakens the claim behind ten long-open problems solved: how many were still, in the relevant sense, open? The non-sofic group is a case in point (Footnote 9).

Note that the claim is about independence, not about the indispensability of researcher in mathematics see § 1.3.3. What is mainly at issue is not the correctness of the proof - which is or isn't independently of the reader - but the inference from them to a capability.

This is Goodhart's law 11, and here it is not a metaphor: the measure is itself the product being sold.

Generative systems are especially exposed to this issue: they are ungrounded, and the party with the financial incentive to optimise the measure is the party producing it.

1.2.3 Capability rests on context. On capability itself, our assessment is plain. A year ago, LLMs behaved in mathematics like badly educated students. They have since been very well trained, and can now identify wrong directions of thought and good directions for problem solving. But their contribution stays narrow in scope 12 and still rests on context previously built - the definitions, the libraries, the accumulated understanding. Whether that limit is conceptual or merely a matter of engineering, we do not know, and we would not bet against scale: nothing we know of prevents a system from proposing its own definitions see Footnote 2.

Working mathematicians are already wondering where the reach can stops:

There are many who will argue that AI is going to come up with genuinely new ideas that people have never thought of before. I don't know that I believe that [. . . ] But the ideas are somehow already there.

- K. Ono [Ono26]

The reason is structural. A model is placed to digest a corpus of ideas and results no person can read - a researcher covers under 0.1% of it in a working lifetime - and to harvest what is already standing in it; at that scale, harvesting and creating become indistinguishable to the non-expert, for whom the research frontier is invisible in any case 13. And harvesting a corpus is not producing one. An age of gleaning rather than of discovery?

Suppose the doubt is misplaced, and that machines do come to choose the notions. The concession costs the argument nothing. If machines come to choose the notions, what changes is who chooses - not that choosing is the scarce act. Someone must still recognise a good choice as good. One might reach for a trained notion of 'goodness', but a trained ranker optimises an existing proxy, while mathematics favours a notion on which one can build - and that is settled downstream, not at ranking time. It is that recognition, that judgment, not the generating, that this essay is about.

Whether or not they one day generate their own context, the question will remain that of the human-machine interface: its nature, and its quality (§ 3).

1.3 The economics were already wrong

Residue and product · public good · externality · the unfunded ecology · mathematical capitalism

1.3.1 No one ever worked out how to buy it. The economic story about mathematics was wrong before any of this. We are funded as if theorems were the product, and we sell teaching as the justification. Both are residue 14. The product is human understanding - and no one ever worked out how to buy it 15.

The distinction is not that the theorem is worthless - it is the instrument of transmission - but that what it transmits is a capacity to think that must be rebuilt in each reader ; the writing, the seminar, the refereeing are that rebuilding, and none of it is what the theorem states. And the residue does not only transmit: it orients. A conjecture is pure residue - countable, publishable, and not even proved - yet its whole office is to make a horizon visible, so that someone knows where to look next; that is the arc Figure 1 draws, from the residue through understanding to the choice of the next question.

Tab. 1. Residue and product. The claim of this essay is the last row: AI drives the marginal cost of the left-hand column towards zero, and thereby makes the right-hand column visible, for the first time, as the scarce thing.

One case is worth having in full, because the institution counts it only as overhead, and because the researchers themselves rarely notice it either: the preparation of a funding application. Written as science rather than as a bid, it yields a research programme ready to be carried out - by the funder's own survey, half the programmes of unsuccessful applications are carried out all the same, on other money. The application was refused; what it produced was kept.

The figures are not small - the mathematical sciences are credited with £495 billion of gross value added in the United Kingdom, and with about one job in eight there and in France alike [B] - and yet the membrane between what we understand and the economy has always been close to impermeable.

AI has not created this problem. It has called the bluff, because it can mass-produce the residue (Table 1). What it cannot produce is the reason anyone wanted the residue in the first place.

1.3.2 Calling the bluff. The bluff was, in fact, already on public record. In 2019, Japan's ministries of economy and education published a joint report under the remarkable title The Coming Era of Mathematical Capitalism [MM19], which names the country's top three priorities for science:

- METI and MEXT (2019)

It observes that the corporate race in AI 'requires human resources with a higher knowledge of mathematics,' and asks - explicitly, and without answering - what 'management or social system' would suit such an era. The question of our social contract is thus not a private anxiety of mathematicians; it is an open item on the books of governments.

Five years on, the same ministry is funding an attempt at an answer: a CREST area opened in 2024 under Motoko Kotani, Creation of Mathematical Foundation for Prediction and Control, whose stated aim is to 'build a new social infrastructure' on the basis of mathematical prediction [Jap24] - a structure rather than a project (§ 2.3.3).

Behind both the question and the attempt is a single change: the membrane between what we understand and the economy, always close to impermeable, has become permeable in both directions - mathematics is drawn into the economy as a priced input, and economic demand now reaches back into what mathematicians are funded to do. That is, the traffic is priced.

From a broader societal perspective - with the economy as one of its parts - what crosses the membrane is the portion of the good that carries a price; what still stays behind is the rest - a public able to read and integrate what its machines produce, the slow formation of people, a cultural shift. When does the greater part begin to cross?

1.3.3 The externality, and the non-rivalry of the corpus. The new arrangement gives the old imbalance a precise name.

Responsibility for correctness is the cheap half, and it is now machine-dischargeable; the expensive half - reading, situating, repairing, teaching, turning a correct proof into something that can be built upon - is left to us, researchers, and takes years.

That is an externality in the ordinary economic sense: extremely well-capitalised consumers; an unfunded ecology of researchers who keep understanding alive ('maintainers', says the software idiom - a word that fits the libraries and undersells both the people and the collective intelligence), still needed, by OpenAI's own admission (§ 1.2.2) - see also the AI training requirements of § 1.3.3; and infrastructure that rots quietly.

But an externality is only an argument if it names an instrument; ours would be structural rather than fiscal, and we return to it in § 2.3.

Two things in particular are consumed and neither is paid for. And here the economics is, unusually, on the argument's side: what is known of the returns to basic research places them in people and their accumulated understanding, not in the results they publish - the residue and the product, under an older name; non-rivalry is why the corpus, not the theorem count 16, is the asset. The first is the corpus: not the literature, but the digested, exposited, taught mathematics the models are trained on, which took centuries to build and which does not deplete by being read. But non-rivalry holds of the stock, not of its provision : what depletes is the pipeline that keeps producing and digesting it - the finite attention of the people who expose, referee, canonise and teach. It is a different kind of good, and the one actually under pressure [C].

The distinction is not academic, and the companies discovered it empirically: Practicioners report that AI training on the published literature and on forums like MathOverflow underperformed - though both are already digested for human readers - and AI companies found they had to commission new corpora, written by mathematicians for the purpose. For LLMs as well, the digested layer is not a by-product of publication; it has to be made, by people, deliberately.

The second is the measure - what $2,000 buys is evidence of capability, and that evidence is only worth something while the community certifying it still functions (§ 1.2). This is not a guild claiming to be indispensable: it is the ordinary requirement of any science that a measure be certified independently of the party it measures. Kernels check proofs - imperfectly, and only proofs: whether a statement says what was meant (§ 2.1), and whether ten instances warrant a claim about a system, no machine certifies.

Which raises the question to put to the ecosystem rather than to the models: can it produce understanding, economically and culturally, with no researcher in the loop, when its targets are whatever can be measured?

An oracle answers; a science explains - one should not trade the second for the first without noticing.

2 The audit and the structures

From what is produced to what can be required. Mathematics can verify without asking anyone's permission, which is rarer than it sounds, and it can therefore put questions to whoever announces a result. What it cannot do alone is build, fund, and hold open the structures on which that capacity depends.

2.1 The asymmetry, and the audit

Verification without permission · formalisation · Lean and Mathlib · training data · attribution

2.1.1 Verification without the producer's permission. What follows from the means of production belonging to someone else (§ 1.1) is not only a question of which interface gets built, but of scale: an asymmetry of manpower and of compute that no university can match. This is serious for a field with a culture of openness and the cheapest science there is: a person, some paper, access to a library 17... some mathematics!

Mathematics, however, is the one field where that asymmetry has a technical answer rather than a negotiated one. Every other discipline that wants to check an AI company's claims must ask the company for access; the weights and the compute are theirs, and access can be withdrawn quietly, without anyone breaching an agreement. We do not have to ask (Table 2).

A proof - written or formal - can, and must, be checked independently of the prover: it has always been the rule of the field. No API key, no compute parity, no permission.

The volume of machine production is a genuine difficulty, and this is where formalisation enters: machinechecked proofs, open source, carried by communities such as those behind Lean and its library Mathlib [The20], or Rocq (formerly Coq), Isabelle and Agda. It is the one form of refereeing that scales with machine output, and it makes hallucination detectable - at the level of the proof. But refereeing was never only error-detection, nor the certification of some absolute truth: it is also how a field digests a result - how one person's argument is read, situated, and made part of what everyone can build on. A kernel scales the first office and not the second 18.

At the level of the statement, matters are different: no kernel can check that a formal statement says what the mathematics meant. The accident report of [LS25, § 5] is instructive - the authors relate discovering, mid-project, that a kernel-accepted statement was not the theorem they had meant to prove; a Lean evaluation convention, under which functions silently return 'junk' values outside their domain of definition had changed the content of the statement, while leaving every proof valid - see also [KT26, § 4.4]. 19

But formalisation can also work the other way: in economic theory, formalising Aumann's agreement theorem - fifty years old in 2026 - made precise what it means for two parties to hold 'the same priors', a hypothesis whose subtleties had gone unexamined [Ono26].

Either way, the same conclusion: whether a statement says what was meant is not something a kernel settles, and formalisation can at best expose it. That is a question for people - which is what the next section asks.

2.1.2 Our asset is their raw material. There is an irony here worth stating plainly. The property that makes formalised mathematics auditable - that a proof can be checked by a kernel, with no human in the loop - is exactly the property that makes it valuable as training material for LLMs.

The Leiden Declaration says so without euphemism: what makes mathematics attractive to general-purpose AI development is that 'the correctness of formalized proofs can be checked automatically, without the need for human oversight,' which yields 'an effectively unlimited source of feedback for training' [Por+26]. The same property that lets us audit them lets them mine us.

This is not an argument against formalisation. It is an argument for noticing that our defensive asset is also somebody's raw material, and for asking on what terms the library is being read.

2.1.3 Why do we cite? Attribution is a different matter, and deeper than an acknowledgement of debt. Why do we cite? Not to pay persons.

Wecite prior works as lighthouses: they mark where understanding advanced - the progress, the techniques, the context that cast light and what it lit - over a landscape still being charted. Models are trained on the published commons and, as the same Declaration observes, 'frequently return outputs that do not properly cite the human works they synthesize' - on data often obtained by 'systematically exploiting licenses and access arrangements that were not made with artificial intelligence in mind' [Por+26]. No kernel adjudicates attribution, and here we are exactly as exposed as every other discipline.

What is lost is not credit: an output without lighthouses flattens the landscape, and a landscape without relief offers no journey - nothing to steer by, nothing worth travelling to. Three of the questions below establish whether a claim is sound; only the fourth asks whether the field can build on it.

2.2 Four questions for an announced result

Disclosure · who chose the problem · independent evaluation · First Proof · EMS Code of Practice

2.2.1 Whoever makes the announcement. Hence the questions we should put to any announcement of a mathematical result, whoever makes it - AI company or individual - written or formal:

• Is the complete argument public - the understanding, not only the residue?

• Who chose the problem, and the terms in which it is stated - and when?

• What independent checking process has been applied?

Tab. 2. Who can check whom. Mathematics is the only row whose verification does not require the producer's cooperation, and the only one with a form of refereeing that scales with machine output. The 'yes' holds at the level of the proof; at the level of the statement it does not.

• Who closes the loop - is there a named interlocutor, and terms under which the field can read, question, attribute, and build on the result?

The four bind an individual exactly as they bind a laboratory. The fourth, however, answers itself in one case and not in the other - someone announcing their own result is the interlocutor, and can be written to; an announcement issued by a company - as in the case of the solutions to ten long-open problems § 1.2.2 frequently has no one behind it at all, which is the open loop of § 3.1. 20

In the formal case 21 this also becomes precise: who wrote the formal statement, and was it fixed before the model started? If one system produced both statement and proof, the verification establishes mostly internal consistency - ground for suspicion rather than reassurance about the claim itself.

2.2.2 The third question, institutionalised. Something answering to the third question already exists. First Proof [Fir26] is an academic-led nonprofit that benchmarks AI systems on research-level mathematics, its editorial and governing boards drawn from Stanford, Berkeley, Harvard, Yale, Columbia, Chicago, UT Austin, and EPFL/Imperial College London.

In its 'First Batch' project [Abo+26], it evaluated problems in a range of fields, under controlled conditions, with expert refereeing for correctness and for exposition: of the ten problems it set, seven were solved at publication-level quality, at a compute cost between $10 and $1,000 apiece. The shape of the announcement echoes § 1.2.2; what differs is who ran it.

The score is not the interesting output. The evaluation was designed and run by the people qualified to referee it, rather than reported by the party being evaluated the third question, institutionalised.

2.2.3 The standard already exists. None of this is a demand invented for the occasion. The European Mathematical Society's Code of Practice [Eur25] already instructs mathematicians not to make public claims of new theorems unless full details can be provided in a timely manner.

And the extension of that standard beyond the profession is no longer a private view: the Leiden Declaration calls on collaborations between mathematicians and industry to abide 'at minimum, by the standards we expect of our colleagues' [Por+26]. We are asking no one - company or individual - for more than the standard mathematicians bind themselves to.

Questions and standards, however, only bind where the two sides actually meet (the fourth question). What remains is to build, and to fund, the places where they do - the structures, to which we now turn.

2.3 The structures are the story

Interfaces · dependency at scale · open code and publication · evaluation and corpus · sovereignty · fund structures, not projects

2.3.1 The two sides are not symmetric. Interfaces are now being built from two sides, and they will outlast any individual result: (i) From the companies: OpenAI's ChatGPT for Academic Researchers offers free model access to a hundred thousand scientists [Ope26], Google DeepMind's AI for Math Initiative opens its most advanced tools to five partner institutions 22 - access at scale on one side, access by selection on the other; (ii) From academia: First Proof, expMath, Mathlib, and a growing set of instruments built by the community rather than borrowed from outside 23. 24

The two sides are not symmetric, and the asymmetry cuts both ways. Free access at scale is dependency at scale, not a research partnership: access is granted, and can be withdrawn without anyone breaching anything (§ 2.1), only now with a hundred thousand people downstream of the decision. In the other direction, two things sit on our side of the table and not on theirs.

The first is the evaluation:

A capability claim is worth what its certification is worth, and the certification is ours - designed, run and refereed by the community, see § 2.1 - The asymmetry, and the audit.

The second is the corpus, which academia does not merely hold but produces and keeps legible - the definitions, the libraries, the expositions, and the people who write them. Each side is short of exactly what the other holds.

That is a negotiating position, and a better one than the current mood suggests - a mood that presses for close collaboration and calls it symbiosis. It holds only if we notice what is actually being settled now: the structures, not the individual results.

2.3.2 Interface-structures: the form is not the practice. Between these two sides, however, a third kind of structure is emerging: interface-structures, neither corporate laboratory nor university department Axiom Math or MathInc among them, a company in the older sense of the word 25 rather than in the sense these pages have so far had to give it. They hire doctoral students, early-career and senior researchers; they build new interfaces of knowledge, integrating AI capabilities, for sound and fast progress in understanding. What they need from academia is recognition, funding and partnership - an alternative to sending our people to the companies, not an outpost of them. That anchor is what makes them interface-structures rather than laboratories: without it, the incentive is to capture the recognition and leave the corpus-work to the community that has to live with it.

The form, however, is not the practice. A structure of this kind can produce work a field can build on, or it can produce volume the field must then clean up: formalisations no one can read (or rather digest), results with no way into the literature (or no way to contextualise). Which of the two it produces depends on the anchor - representatives of academia with the standing to say what would count as usable, and answerable for having said it.

It depends, too, on what leaves the structure. Open code, open publications, and open access to new tools for results that anyone can ingest and digest. For two out of three, that is already the practice of the instrument the community has built 26 - and it is what keeps an interface-structure an interface rather than a gate.

Accepting such structures as partners is not a courtesy; it is the condition under which what they produce can be built on at all.

2.3.3 The unit to fund is a new type of structure. If there is an instrument here, it is complementary to the ones we have and not a rival to them 27. That instruments of this kind can be made well is not in doubt: the European Research Council funds a programme and a person rather than a deliverable, and a generation of European mathematicians owes to it the freedom to choose its own questions. It did not price the product - no one has - but it stopped requiring the residue in exchange.

What no agency produced is expMath, Axiom Math, MathInc or Mathlib, which emerged outside the academic frame - a gap in the catalogue of instruments, not a fault in any of them. The agencies have since begun to answer in their own form, anchored in academia: the NSF's Institute for Computer-Aided Reasoning in Mathematics (ICARM) opened in 2025 [NSF25], and the CREST area of § 1.3.2.

Designing a structure has not, until now, been the mathematician's business: the social contract gives us teaching and research, and delegates structuring to agencies. This is changing from both ends: the agencies are building institutes, and mathematicians are now among the founders of the new interface-structures. The direction can therefore be stated from the inside, as it should be.

Two interfaces have a claim on such instrument. The newest, where academia and AI companies genuinely meet rather than transact, has still to be built: the new institutes are anchored on the academic side, and it is the crossing that is missing. That crossing is the natural place for the externality of § 1.3 to be internalised - the ecology funded where the corpus and the evaluation are actually produced, the people, not only the libraries they maintain. The oldest is education, which produces the value of the next generation rather than of the next quarter - including the capacity to use these tools well - and which therefore needs money on a clock that is not the quarter's.

Both are questions of sovereignty and of culture as much as of economics. A country that stops training the people who can read and integrate what the machines produce has outsourced rather more than its compute.

The unit to fund is the structure : projects and individuals are countable, which is precisely why they are the ones we do.

3 The ecology of the journey

What all of this does to the work itself, and to the people who do it: the loop that constitutes the profession, the training of those about to enter it, the mismatch between the speed at which results are produced and the time understanding takes to form, and the one thing in the field that was never reproducible. These are questions of morale as much as of production.

3.1 The loop is the profession

The discovery loop · judgment · human-machine interface · open loop · doctoral training

3.1.1 The fear, and the two cuts. A widely shared fear - vividly put in a recent essay by a young mathematician [Ham26] - is that the profession survives only as a taste-labelling layer: paid 'to optimize the weights for 'interesting', 'beautiful', anything you like,' permitted to comment and appraise, forbidden to create.

The same suspicion arrives at the other end of a career.

If my success as a mathematician relied only on my ability to learn techniques that somehow could be put together to prove a theorem, then maybe that was actually automatable, and maybe I mistook all of that hard effort for something maybe it wasn't. - K. Ono [Ono26]

What he had been doing instead, he says, was

I was learning how mathematics fits together to help me become a mathematician who can ask these questions and participate in the discovery.

In both, the same displacement: what the profession counted turns out to be the part that automates, and what it never counted - learning how mathematics fits together is what made the mathematician. And in both, the same unspoken premise: that appraising and discovering are separable jobs, one of which can be kept while the other goes.

The fear admits of a mechanical answer. Discovery and the weighting of 'interesting-beautiful' are not two jobs but two moments of a single loop: understanding tells us where to look, and looking is what produces understanding. The loop is the profession. Cut it, and the damage arrives at both ends at once: at the output, checking and cleaning up after the machine; at the input, labelling and weighting with no discovery of one's own (Figure 1).

The loop is drawn for one person; the collective understanding is not a larger loop but the ground the loops share: a notion belongs to the field when it can be used and re-walked by any of us. The residue is what travels between loops; the journey is what cannot.

How does one label where to look, once detached from the understanding that alone tells us where to look?

3.1.2 The open loop. The ten problems of § 1.2 are a live specimen of that cut, and of what falls through it. At the input, there is no co-author. There is a published narration of the model's reasoning, which one can read but not question: nobody to write to, nobody to invite to a seminar, nobody who can be asked why this direction and not another. A narration is a record of a path, not a partner on it.

At the output, the contribution to understanding is real but in its weakest form: what Thurston calls a collection of 'answers', where what people wanted was understanding [Thu94, § 1]. The result is correct, documented - and still to be converted. That conversion, which is reading, situating, exposing and teaching, is years of work; it is ours; and nothing in the announcement funds it 28.

Fig. 1. The loop is the profession. Understanding tells us where to look; looking is what produces understanding. Machines are now strong over one quarter of the circumference - and not over the quarter that feeds it. The taste-labelling layer is this same loop cut at the two points where the human meets the machine.

So the proofs are correct and the loop is left open - and an open loop is not a slower loop, it is a different object.

3.1.3 The loop kept whole: a new practice. The same loop, kept whole, points the other way. AI is a formidable trainer of intuition for reaching new research frontiers: a doctoral student can test an intuition and build new understanding in afternoons where it used to cost months - and so can any established researcher investigating outside their own field. Learning that one asked the wrong question was the most expensive lesson in a mathematical education; it is now nearly free.

The change is not only one of tempo but of the nature of the work itself. Ingesting and digesting - reading and writing - have long been dissociated acts, separated by months and often by years; the AI tool brings them into contact, so that one questions while reading and tests while writing. A new instrument makes a new way of working before it makes a new result. The same instrument works at the other scale: a result can now reach, and be questioned by, more people - and other people - than any seminar could hold (Coda).

What practice maintains, and a labelling layer cannot, is judgment - whose deep form, in fundamental mathematics, is the choosing of definitions (§ 1.2).

'Knowing where to look' is not a stock that can be harvested; it is maintained by practice.

Severed from practice, the layer degrades: the arrangement the fear imagines fails on its own terms.

Until now, nobody funded question-asking; it produces nothing you can count. AI may change that: once the countable part costs nothing, the scarce part finally carries a price and acquires a value our socio-economic system had so far never assigned it.

3.2 Students get closer to the research frontier

Doctoral training · pre/post-training · division of labour · computer algebra, a precedent · no collective position

'What is a mathematician trained to become, once the countable half of the work no longer needs one?'

The question is not hypothetical. It is being answered already, month by month, in the thesis topics proposed and the positions offered to those starting out - and it is answered first for the people with the least say in it.

3.2.1 Not at the beginning of the loop. The danger is not the tool but the routing. The next generation is being pushed toward the two countable ends of the pipeline - the ends that are easy to fund and easy to measure - and those are precisely the stretches that train no judgment.

The AI labs have names for the two ends: 'pre-training' and 'post-training' 29 - feeding the machine a corpus, then cleaning up after what it returns. Put a doctoral student at either end and one has built the taste-labelling layer of § 3.1 in advance, out of the people who were supposed to go round the loop in their turn. Such a layer does not degrade, as § 3.1 has it: it never forms.

On this point, we stand in opposition to the 'increasing division of labor' of [KT26]:

One can envision an increasing division of labor in the future of mathematical research: [...] any given mathematician may increasingly specialize in just a few aspects of this process, for instance focusing on utilizing AI assistants to prove results as directed by some more senior member of a research group, or on using the most recent literature [...] to propose new directions of inquiry.

- T. Klowden and T. Tao [KT26, § 4.6]

Specialization at each side of the loop is the loop cut at both ends, and made into a career structure.

A mathematical laboratory worth building is one in which each member is fully integrated and goes round the whole loop - not one in which each is assigned an arc.

The objection is not to formalisation. It is a genuine competence, and the students who acquire it are not wasting their time: the objection is to formalisation as the whole of a formation - the French word for what training has lost: preparing someone to digest the competences no one can yet name, rather than equipping them with the ones we can.

Astudent who has never wandered the landscape has no way of learning that a question was the wrong one.

3.2.2 Classical training first, then contact, fast. Students still ask for a classical training, and are right to: definitions made by hand, proofs written out, the long slow reading. Reasoned use of the machine builds on that; it does not substitute for it.

But the two ends of the pipeline are not the only place a student can be put. Contact must come early, supervised, and in three staged forms rather than one:

• Corpus. Learning to read, and to ingest, at a scale no one could read before - the machine as a way into a literature. This is where the overhang of § 1.2.2 is met rather than described.

• Acceleration of experience. Testing an intuition in an afternoon instead of a term: learning that the question was wrong, cheaply.

• Investigation. The student's own question, with the machine inside the loop rather than at its ends.

The order is not decorative. (2) without (1) produces fluency without reading; (3) without (2) produces confidence without calibration; (1) without (3) produces a reader who never asks. In each case, scientific progress is impoverished, if not entirely absent.

3.2.3 The profession has already run this experiment: the 90's computer algebra. Nothing here is a new anxiety: the last time a machine entered mathematics, the same two failures were available.

When computer algebra arrived, the practice could have collapsed into (a) a toolbox of computations and low-level programming, or (b) a practice of pure first-order logic 30. Neither would have produced a mathematician. What it produced, when it worked, was a new paradigm of scientific thought - experimental mathematics - and a generation that is able to think with machines rather than through them.

The remedy is practical, not curricular. Judgment of that kind cannot be lectured into anyone: it is maintained by practice, and by nothing else. Hence the arrangement to build: the student in front of the machine as early as possible, and supervised - the one place where taste is called for, and therefore the one place it forms.

Here we part from Bessis [Bes26], for whom the frontier between teaching and research is sharper: in our view machine practice blurs it, bringing students into contact with the mechanisms of research earlier than any curriculum could.

Teaching as before is no longer possible, and no collective position exists - no department, no learned society, no funder has one. The new practice is being developed, and valorized, in the new structures (§ 2.3.3); what is experimented there will percolate into academia - which is how a practice becomes a formation.

3.3 Compression is not acceleration

Rate problem · proof abundance · company time vs. generation time · Thurston on foliations

3.3.1 From proof scarcity to proof abundance. AI compresses the stages of the work that can be counted - from an open problem to an argument on the page. As the tools are use now, they leave untouched the stage that follows: the one in which a result is read, situated, exposed, taught, and eventually becomes part of what the field simply knows - the closing of the loop 31. That is how they are used, not what they can do: turned the other way, the same instruments lower the cost of entering a field instead of raising the volume it must absorb (Coda).

As Terence Tao (Fields Medal, 2006) states it plainly, if no 'suitable policy and cultural changes' are made:

Abundance is not, by itself, progress. The fact of a result travels cheaply; the horizon it opens does not. A thousand results nobody has travelled to will open little more than the fact of themselves.

Compressing the countable stages does not accelerate understanding; it widens the distance between what exists and what is understood.

Fig. 2. Time compression of generation is not, by itself, acceleration of understanding (schematic). One turn of the loop, from an open problem to a result one can build on. The angle is each stage's share of the turn; the radius is how long the turn takes, so nearer the centre is faster; the thicker the ring, the more broadly the understanding is held.

Machines compress the early stages in every case alike - but only where the closing stage is carried out does the turn shorten. Left open, it never closes at all: compression of the early stages alone cannot reach understanding.

3.3.2 What AI can shorten, and what it cannot. A field can move faster and understand less, at the same time. Economists have a name for the missing quantity: absorptive capacity, the ability to use knowledge produced elsewhere, built only by doing research oneself [CL90] - which is why free access to results confers little on a community that has stopped producing the people who can read and integrate them (§ 2.3).

Properly grounded, and held to the code of practice of the mathematical sciences (§ 2.2), AI can however raise that capacity - the rate at which frontier work can be taken up - by enhancing individual practice. The distinction matters: becoming standard is slow because it requires broad deliberative consensus, and AI does not speed deliberation.

What AI can shorten is each participant's climb to the point of being able to take part.

3.3.3 A mismatch of clocks. Underneath is a mismatch of clocks. Company time is release-cycle time; understanding takes root on the time of a generation. The two cannot be brought into phase by working harder at the fast end - which is the only end anyone is currently paying to speed up.

Nor is this a machine problem in origin: the precedent is at human scale and required no AI. Thurston's first subject was foliation theory, and his flood of results emptied it within a couple of years. Colleagues were advising one another not to go into foliations - Thurston was 'cleaning it out' - and told him, not as a complaint, but as a 'compliment', that he 'was killing the field'. He is explicit that the territory was not intellectually exhausted; what the rate of production destroyed were the ecological conditions of the subject, the ones under which anybody would want to keep thinking in it [D].

A rate of production can destroy the conditions of understanding. It is a rate problem before it is a machine problem - and it now has a very much larger engine attached to it.

3.4 The decision is ours

Priority vs. journey · Library of Babel · reproducibility · authorship · what cannot be mass-produced

3.4.1 Priority, and the journey. Aworry one hears from the next generation of researchers [Ham26] has the shape of the Library of Babel - Borges' library that contains every possible book, hence, somewhere on its shelves, every theorem, every proof, every refutation, already written. But that is already our condition: every researcher assumes that any result they obtain could be obtained by another trained mathematician.

Is the experience of discovery being foreclosed? To answer, one must split 'discovery' in two. One sense is priority - first place in the world's ledger. That, machines will indeed make scarcer and noisier. The other is the journey - the personal passage from confusion to understanding - and it is indexed to a person, not to the ledger.

3.4.2 Nothing is lost. The residue was always reproducible; the journey never was. Here the essayist quoted above puts it exactly right: 'human mathematics is Talmudic' [Ham26] - the charge of learning comes from being conversant, across centuries, with the person who discovered. But then the conclusion inverts: if meaning travels through human authorship, the accumulated corpus - the thing we spend our lives learning and teaching - loses nothing to anything a machine proves afterwards.

Each of us adds a little to a great deal that was already there: almost everything one will ever understand was discovered by someone else, and that has never once made the understanding less ours. For understanding is collective only in the way it is kept alive: not stored but re-walked - each journey rebuilds a piece of the shared corpus in another mind 32.

That is why a machine's proof, which enters only the ledger, adds nothing to what the field actually understands: the shared understanding lives only where someone has made the passage again.

3.4.3 What is actually at stake. The channel of discovery is not being sealed. It has become crowded and noisy - not a bad problem to have, and one we already build for: curated libraries, large collaborative interfaces, machine-assisted formalisation.

What is genuinely at stake is not on the ledger at all - and it is a decision, not a fate.

The journey cannot be mass-produced - and a collective understanding lives only where the journey is made. But it can be routed away, defunded, traded for what can be counted. That decision is ours, not the machine's.

A decision of that kind shows itself in budget lines, in what a committee agrees to count, in the positions offered to people starting out - and it is announced, plainly enough, in the collaborations struck with the new interface-structures (§ 2.3).

The journey, then, is not a private consolation; it is the piece the rest of this essay defends: what closes the loop (§ 3.1), what the rate endangers (§ 3.3), and what the audit and the structures of § 2 exist to keep funded.

Coda

The models will keep producing mathematics, and mathematics will keep absorbing new modes of production, as it always has. The open questions do not belong to the machines: who checks, who trains, who pays - and whether we continue to organise, and to fund, the one experience that was never reproducible in the first place.

Fig. 3. The virtuous loop. People choose which questions are worth the asking; machines produce at a rate no community could sustain; the kernel makes what they produce checkable without its author having to be trusted, which opens the door to whoever's argument checks. Researchers integrate what arrives into the understanding and only that arc, the return to judgment, closes the loop.

A virtuous loop nonetheless becomes available: machines propose at a rate no community could sustain; formalisation makes the proposals checkable without their authors having to be trusted; and, the material now being machine-tractable, the same tools can be turned back on it - questioned, replayed, explained so that expertise becomes something a newcomer builds rather than a barrier already cleared (Figure 3). And once the corpus once grounded by researchers, those tools let far more of them read, question and answer one another than any seminar could hold.

Read against Thurston's case, the virtuous loop lowers the entry cost of high-level knowledge - for a more inclusive and diverse practice.

None of that is automatic: it holds only where the practice is built for it. Such tools can be turned outward or inward: they can prepare more people to take part in a conversation, or they can answer in its place. Which happens is settled by the structures, not by the model.

The 'randomness' from the LLMs, the 'rigidity' from the kernel, and the judgment from people - and the loop finally closes.

Benjamin COLLAS

Researcher at the Research Institute for Mathematical Sciences of Kyoto University (RIMS), working in arithmetic homotopy geometry - a field that reconciles the rigidity of numbers with the flexibility of geometry. He leads the CNRS International Research Network AHGT, which links RIMS, the Université de Lille and the ENS-PSL, and brings together some ∼ 120 researchers in ∼ 15 countries.

Email: bcollas@kurims.kyoto-u.ac.jp Web: https://collas.perso.math.cnrs.fr

Positions and updates on mathematics and AI: http s://collas.perso.math.cnrs.fr/math-and -ai.html

Declaration on the use of AI

The arguments, judgments and factual claims in this essay are the author's own. An AI assistant (Claude Fable 5 and Opus 4.8, Anthropic, accessed via Claude Code, July 2026) was used to draft and restructure English prose from the author's own writing and notes, for copy-editing, and editorial critique.

The author reviewed and revised all text, verified the sources, and takes full responsibility for the content.

Addendum - A release of ∼ 370 notes

In October 2026 OpenAI released ∼ 370 mathematical notes, retractions included. The autumn also brought two announcements: (a) a formalisation by Anthropic of a proof of Fermat's Last Theorem, and (b) a potential solution to Navier-Stokes announced by OpenAI. Each obliged the international community to take a position.

The weeks that followed their publication tested the arguments of this essay. Nothing below corrects the pages above: the episode has altered no argument, it has priced one.

• Grey areas, and why the notes cannot be ignored. One would wish to ignore a release of this kind; one cannot - and not because of OpenAI: 'ghost results' have impeded the progress of mathematics long before any model was trained (Footnote 10). The remedy is ordinary - comment on the content, which is not refereeing it. These notes should neither be refereed nor taken as established results; retractions and mistaken references have already been signalled within the community. Whoever seeks recognition as a producer of scientific research names a corresponding author and submits to journals - and on the exposition on display, the first round would be hard to pass.

• Statements, not results. OpenAI produces statements : not theorems, and not results in the sense of proved statements integrated into the progress of mathematics. Its production accelerates the beginning of the loop while cutting it - the output cannot re-enter as input for building new mathematics, by machine or by human. This is the open loop of § 3.1, at a volume of several hundred. On this record - Navier-Stokes, the earlier invitations to events on using AI for mathematics, an advisory group on mathematics and AI 33 - whether OpenAI can be considered a producer of mathematical research is an open question.

• The misalignment is at the statement, not at the proof. Verification does no more than it says: it guarantees that the proof demonstrates the statement as written, not that this statement is the one anyone wanted (Footnote 19). Who chose the problem, when, by what procedure, and what the result contributes all require an external evaluation, by mathematicians (§ 2.1).

• Provenance: who chose the problem, when, and on whose work. On Navier-Stokes the paternity question is contested outright (Footnote 20); and it reaches back into the counterexample of § 1.2, which follows, in content and in notation, a PDF file of Borisov-Gabber-Vasiu - prior work the production does not acknowledge. An output without lighthouses is not only a failure of credit (§ 2.1): it is what makes an evaluation hard.

• The cost of externalisation, priced. The relationship established with mathematics is one of externalisation -the cost of production shifted onto an external entity - and of depletion, not of the corpus but of the pipeline that provides it (§ 1.3.3; the value consumed is our time). The legitimate support is therefore not the organisation of events but funding positions : at three years of position for each note released, this release prices at over a thousand position-years, or some $90 million 34.

• What suffices is a seminar. Given the mathematical quality of the notes, a Zoom seminar is more than sufficient and costs nothing: the AHGT Taming the flow seminar was convened for precisely that 35. Set beside what CNRS, DFG or private partners (of IHES, MSRI, etc) bring, the record does not warrant support for event organisation. As for the idea-sketches the notes contain, only manuscripts written by groups of mathematicians will properly reflect the mathematical nature of this production - with a footnote recording the origin.

• Open weights, hosted by institutions. The encouraging development of the autumn is on the academic side of § 2.3: institution-hosted open-weight models (Footnote 24). Access that cannot be withdrawn is a different good from access granted at scale.

There is a diversity of mathematics, hence of practices and of evaluations; answers to these issues are not canonical. Positions taken as the situation moves are kept, with their sources, on the author's page 36.

Notes

• [A] From this perspective, it should be no surprise that the book of nature 'is written in the language of mathematics' (Galileo 1623) - or closer to us, that the advanced theory of topos is applied to AI (2025). For a debate on the end game of fundamental mathematics or its utilitarianism, we refer to a 1830 comment from Carl Gustav Jacobi (result of Humboldt's mathematics as reine Wissenchaft as a source of freedom and personal realisation) to Joseph Fourier (the Polytechnicien of the French revolution, for which Mathematics as a state instrument is required) - see [JL75]

Fourier avait l'opinion que le but principal des mathématiques était l'utilité publique et l'explication des phénomènes naturels ; mais un philosophe comme lui aurait dû savoir que le but unique de la science, c'est l'honneur de l'esprit humain, et que sous ce titre, une question de nombres vaut autant qu'une question du système du monde.

The maxim comes a few months before the opening of the Liverpool-Manchester steam railway (Sept. 1830), which set off the Railway Mania of the 1840s, and, with it, the globalisation of the industrial revolution.

• [B] Orders of economic magnitude - with the caveat that such studies measure the economic activity mathematics enables, not the value it produces. In the United Kingdom, the mathematical sciences were credited with £208 billion of gross value added and 2.8 million jobs for 2010 about 16% of GVA and 10% of employment [Del13] - and with £495 billion and 4.2 million jobs, 13% of UK employment, for 2023 [Aca24]. In France, the corresponding study puts the share of GDP impacted by mathematics at 18% and the jobs at 3.3 million, 13% of salaried employment, on 2019 data, up from about 16% and 2.4 million on 2012 data [CI22]. The trend is the interesting part; so is the fact that none of these studies attempts to price what this essay calls the product.

• [C] Economists have treated basic research as a public good since Nelson [Nel59] and Arrow [Arr62]: non-rival, non-excludable, and therefore privately under-supplied - the standard argument for funding it publicly. Non-rivalry is also the engine of endogenous growth theory, in which the accumulation of ideas rather than of capital sustains growth [Rom90] - which puts the corpus, and not the theorem count, at the centre of the economic story. The review literature adds something more useful here. Surveying the evidence, Salter and Martin [SM01] find that the benefits do not travel mainly through the published result: they sort them into six channels, of which (1) codified knowledge is only one, the others being (2) trained people, (3) new instruments and methods, (4) networks, (5) problem-solving capacity, and (6) new firms.

That is, in an economist's vocabulary, the distinction this essay draws between the residue and the product, the limitation of problem-solving results, and the requirement for funding new integrated structures. A non-specialist's question follows: if most of the return travels through people rather than through results, what becomes of the return when the results are free and the people are not funded?

Elinor Ostrom (Nobel Prize in Economic Sciences, 2009) answers by re-typing the good, correcting Samuelson's dichotomy: 'rivalry of consumption' becomes subtractability of use, and a fourth type appears - the common-pool resource, subtractable like a private good and hard to exclude from like a public one [Ost10]. The corpus is not that good; its provision is. What depletes is the pipeline, drawn on a finite pool of expert attention from which no one can be excluded - see also Footnote 27 of § 2.3 for some structural consequences.

• [D] Thurston's account, in [Thu94, § 6], deserves quoting at length. Having 'fairly rapidly proved some dramatic theorems' as a graduate student:

An interesting phenomenon occurred. Within a couple of years, a dramatic evacuation of the field started to take place. I heard from a number of mathematicians that they were giving or receiving advice not to go into foliations - they were saying that Thurston was cleaning it out. People told me (not as a complaint, but as a compliment) that I was killing the field. Graduate students stopped studying foliations, and fairly soon, I turned to other interests as well.

On the cause: 'I do not think that the evacuation occurred because the territory was intellectually exhausted there were (and still are) many interesting questions that remain and that are probably approachable.' He names instead two 'ecological effects': a high entry barrier, his results being 'documented in a conventional, formidable mathematician's style' that 'depended heavily on readers who shared certain background and certain insights'; and the absence of anything left in it for anyone else - 'More than the knowledge, people want personal understanding. And in our credit-driven system, they also want and need theorem-credits.'

The remedy he adopted afterwards is the one this section is arguing for: 'In reaction to my experience with foliations [. . . ] I concentrated most of my attention on developing and presenting the infrastructure', publishing definitions and ways of thinking while remaining 'slow in stating or in publishing proofs of all the 'theorems' I knew how to prove', so as to '[leave] room for many other people to pick up credit.'

References.

[Abo+26] M. Abouzaid, A. J. Blumberg, M. Hairer, J. Kileel, T. G. Kolda, P. D. Nelson, D. Spielman, N. Srivastava, R. Ward, S. Weinberger and L. Williams. First Proof. 2026. doi: 10.48550/arXiv.2602.05192. arXiv: 2602.05192 [cs.AI] (cit. on p. 13).

[Aca24] Academy for the Mathematical Sciences. Analysis of the Economic Contribution of the Mathematical Sciences in the UK. £495 billion of gross value added and 4.2 million people directly employed in mathematical science occupations (13% of UK employment), based on 2023 data. Oct. 2024. url: https://www.acadmathsc i.org.uk/publications/mathsci-supercharges -uk-econ-growth/ (cit. on p. 24).

[Arr62] K. J. Arrow. 'Economic Welfare and the Allocation of Resources for Invention'. In: The Rate and Direction of Inventive Activity: Economic and Social Factors. Princeton: Princeton University Press, 1962, pp. 609-626 (cit. on p. 24).

[Avi25] J. Avigad. 'Is Mathematics Obsolete?' In: arXiv preprint arXiv:2502.14874 (2025). doi: 10.48550/ar Xiv.2502.14874. url: https://arxiv.org/abs/2 502.14874 (cit. on pp. 8, 28).

[Axi26] Axiom. Selected Publications. Research and publications from the Axiom team on ArXiv (c. 20 at this date). 2026. url: https://axiommath.ai/selected -publications (visited on 19/08/2026) (cit. on p. 6).

[Bes26] D. Bessis. The Fall of the Theorem Economy: How AI Could Destroy Mathematics and Barely Touch It. Substack. Apr. 2026. url: https://davidbessis.su bstack.com/p/the-fall-of-the-theorem-econ omy (visited on 16/08/2026) (cit. on pp. 7, 8, 19, 28).

[Cas01] P. Cassou-Noguès. De l'expérience mathématique. Essai sur la philosophie des sciences de Jean Cavaillès. Problèmes & Controverses. Paris: Vrin, 2001 (cit. on p. 5).

[Cav47] J. Cavaillès. Sur la logique et la théorie de la science. Written 1942; published posthumously. Paris: Presses Universitaires de France, 1947 (cit. on p. 5).

[CZC26] Z. Chen, Y. Zhao and A. Cohan. 'Measuring the Gap Between Human and LLM Research Ideas'. In: arXiv preprint (2026). eprint: 2607.01233. url: https://arxiv.org/abs/2607.01233 (cit. on p. 7).

[CI22] CNRS and Institut national des sciences mathématiques et de leurs interactions (INSMI). Étude de l'impact économique des mathématiques en France. 18% of GDP and 3.3 million salaried jobs impacted by mathematics in France. 2022 (cit. on p. 24).

[CL90] W. M. Cohen and D. A. Levinthal. 'Absorptive Capacity: A New Perspective on Learning and Innovation'. In: Administrative Science Quarterly 35 (1990), pp. 128-152 (cit. on p. 20).

[Com+26] J. Commelin, M. Jamnik, R. Ochigame, L. Taelman and A. Venkatesh. 'Shaping the Future of Mathematics in the Age of AI'. In: Notices of the American Mathematical Society 73.6 (2026), pp. 480-483 (cit. on p. 6).

[Del13] Deloitte. Measuring the Economic Benefits of Mathematical Science Research in the UK. £208 billion of gross value added (about 16% of GVA) and 2.8 million jobs (about 10% of employment), based on 2010 data. EPSRC and Council for the Mathematical Sciences, June 2013. url: https://www.lms.ac.uk/ (cit. on p. 24).

[Eur25] European Mathematical Society Executive Committee. EMS Code of Practice for Mathematical Publication. On public claims of new theorems and timely provision of full details. 2025. url: https://euromat hsoc.org/code-of-practice (cit. on p. 13).

[Fir26] First Proof. First Proof. Independent evaluation of AI systems on research-level mathematical problems under controlled conditions, with expert refereeing for correctness and exposition; seven of ten problems solved at publication-level quality, at $10-$1,000 of compute per problem. 2026. url: https://1stproof.org (cit. on p. 13).

[Fou26] F. Fournier-Facio. A Torsion-Free Non-Sofic Group. 2026. url: https://drive.google.com/fil e/d/1F1hBzrlGwX42z9hl0cd8SkosqlJcHYGt/view (visited on 05/08/2026) (cit. on p. 7).

[FBG26] A. Freitas Ramos, D. Barros Hulak and R. J. Guerra Barretto de Queiroz. Formal Verification of an Explicit Counterexample to the Jacobian Conjecture. Formal proof development. Archive of Formal Proofs. July 2026. url: https://isa-afp.org/entries/Ja cobian_Counterexample.html (cit. on p. 6).

[Goo75] C. A. E. Goodhart. 'Problems of Monetary Management: The U.K. Experience'. In: (1975) (cit. on p. 7).

[Ham26] K. Hampshire. The Dark Night of Mathematics - What Are We Really Doing? Substack. July 2026. url: https://kirwinhampshire.substack.com/p/the -dark-night-of-mathematics (cit. on pp. 16, 21).

[JL75] C. G. J. Jacobi and A.-M. Legendre. 'Correspondance mathématique entre Legendre et Jacobi'. In: Bulletin des sciences mathématiques et astronomiques 9 (1875), pp. 126-142. url: https://www.numdam.org /item/BSMA_1875__9__126_1/ (cit. on p. 24).

[Jap24] Japan Science and Technology Agency. Creation of Mathematical Foundation for Prediction and Control. CREST research area within MEXT's Advanced Integrated Intelligence Platform Project; Research Supervisor Motoko Kotani, Tohoku University. 2024. url: https://www.jst.go.jp/kisoken/boshuu/r06/t eian/en/top/ryoiki/ryoiki_c01.html (visited on 20/08/2026) (cit. on p. 9).

[KT26] T. Klowden and T. Tao. 'Mathematical methods and human thought in the age of AI'. In: (2026). On what AI does to mathematics - form decoupled from process, and the standing of machine cognition. doi: 10.48550 /arXiv.2603.26524. arXiv: 2603.26524 [math.HO]. url: https://arxiv.org/abs/2603.26524 (cit. on pp. 8, 10-12, 15, 18, 28).

[KR25] P. Kohli and E. Rives. Accelerating Discovery with the AI for Math Initiative. Google DeepMind. Oct. 2025. url: https://blog.google/innovation-an d-ai/models-and-research/google-deepmind/a i-for-math/ (visited on 19/08/2026) (cit. on p. 14).

[Kon26] A. Kontorovich. 'Interactions of AI with Research Math and Formalization'. Virtual presentation;

Notes available at: https://alexkontorovich.wor dpress.com/2026/04/05/lecture-interactions -of-ai-with-research-math-and-formalizati on-at-newton-insitute-cambridge/ . Cambridge, UK, Mar. 2026. url: https://www.newton.ac.uk/s eminar/50271 (cit. on p. 17).

[Lea23] Lean FRO. Lean Focused Research Organization. 2023. url: https://lean-lang.org/fro/ (visited on 28/08/2026) (cit. on p. 15).

[LS25] D. Loeffler and M. Stoll. 'Formalizing Zeta and L-Functions in Lean'. In: Annals of Formalized Mathematics 1 (2025), pp. 43-56. doi: 10.46298/afm.15 328. url: https://doi.org/10.46298/afm.15328 (cit. on p. 11).

[Mat25] Mathlib Initiative. The Mathlib Initiative: Building the Digital Foundation of Mathematics. Strategic support for the Mathlib ecosystem. Renaissance Philanthropy. 2025. url: https://mathlib-initiat ive.org/ (visited on 28/08/2026) (cit. on p. 15).

[Mat26] MathOverflow. What Are the Key New Ideas in the Proof of Nonsoficity of Groups in OpenAI's Construction? Question 513866. 2026. url: https://ma thoverflow.net/questions/513866/what-are-t he-key-new-ideas-in-the-proof-of-nonsof icity-of-groups-in-openai-s-con (visited on 05/08/2026) (cit. on p. 19).

[MM19] Ministry of Economy, Trade and Industry and Ministry of Education, Culture, Sports, Science and Technology. The Coming Era of Mathematical Capitalism - How the Power of Mathematics Changes Our Future. Summary; Industry-Academia Round-Table Discussion. Government of Japan, Mar. 2019 (cit. on p. 9).

[Nel59] R. R. Nelson. 'The Simple Economics of Basic Scientific Research'. In: Journal of Political Economy 67 (1959), pp. 297-306 (cit. on p. 24).

[NSF25] NSF. Institute for Computer-Aided Reasoning in Mathematics. NSF grant DMS 2425401; hosted at Carnegie Mellon University. 2025. url: https://icarm.io/ (visited on 21/08/2026) (cit. on p. 15).

[Ols26] P. Olson. Math's AI Crisis Has a Lesson for the Rest of Us. Forthcoming. Bloomberg Opinion. Aug. 2026. url: https://www.bloomberg.com/opinion/arti cles/2026-08-13/math-faces-an-ai-spiritua l-crisis-it-has-a-lesson-for-the-rest-ofus (cit. on pp. 2, 28).

[Ono26] K. Ono. A 58-Year-Old Mathematician's Life Advice about AI. Interview. EO Magazine. July 2026. url: https://www.eomag.io/article/ken-ono-math (cit. on pp. 8, 12, 16).

[Ope26] OpenAI. Ten Advances in Mathematics and Theoretical Computer Science. Announcement of solutions to ten long-open mathematical problems. 2026. url: https://openai.com/index/ten-advances-in-m athematics/ (cit. on pp. 7, 14).

[Ost10] E. Ostrom. 'Beyond Markets and States: Polycentric Governance of Complex Economic Systems'. In: American Economic Review 100.3 (2010). Nobel Prize lecture, 8 December 2009, pp. 641-672. doi: 10.1257 /aer.100.3.641 (cit. on pp. 4, 15, 24, 28).

[Por+26] J. Portegies et al. Leiden Declaration on Artificial Intelligence and Mathematics. Working group of sixteen; drafted in the eight months following the conference 'Mechanization and Mathematical Research', Lorentz Center, Leiden University, September 2025. June 2026. doi: 10.5281/zenodo.20302944. url: https ://doi.org/10.5281/zenodo.20302944 (cit. on pp. 2, 6, 7, 12, 14).

[Rom90] P. M. Romer. 'Endogenous Technological Change'. In: Journal of Political Economy 98 (1990), S71-S102 (cit. on p. 24).

[SM01] A. J. Salter and B. R. Martin. 'The Economic Benefits of Publicly Funded Basic Research: A Critical Review'. In: Research Policy 30 (2001), pp. 509-532 (cit. on p. 24).

[Sch26] E. Schmidt. The AI Revolution. Reunions Talk, moderated by Alan S. Blinder. Griswold Center for Economic Policy Studies, Princeton University. May 2026. url: https://www.youtube.com/watch?v=yS3rw9 lPIPs (cit. on p. 7).

[Sha25] P. Shafto. expMath. DARPA programme running 2025-2028 to accelerate the rate of progress in pure mathematics. Rutgers University. 2025. url: https://w ww.darpa.mil/research/programs/expmath-exp onential-mathematics (cit. on p. 6).

[AIM24] 'Special Issue on AI and Mathematics, Parts I and II'. In: Bulletin of the American Mathematical Society 61 (2024). Part I, pp. 199-372, April 2024; Part II, pp. 373-524, July 2024, pp. 199-524 (cit. on p. 5).

[Tao26] T. Tao. Mathematics in the Age of AI. Public lecture. International Congress of Mathematicians. 2026. url: https://teorth.github.io/tao-web/slide s/age-of-ai-icm-2026.pdf (cit. on pp. 6, 19).

[The20] The mathlib Community. 'The Lean Mathematical Library'. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2020, pp. 367-381. url: https://arxiv.org/abs/1910.09336 (cit. on pp. 11, 13).

[Thu94] W. P. Thurston. 'On Proof and Progress in Mathematics'. In: Bulletin of the American Mathematical Society 30 (1994), pp. 161-177 (cit. on pp. 5, 16, 24).

[Ven24] A. Venkatesh. 'Some thoughts on automation and mathematical research'. In: Bulletin of the American Mathematical Society 61.2 (2024), pp. 203-210. doi: 10.1090/bull/1834 (cit. on p. 5).

Version history.

• 2026.10.12 Version 3. Addendum on the October 2026 release of some 370 notes: ghost results and why the notes cannot be ignored; statements rather than results, and the loop cut at volume; the misalignment located at the statement and not at the proof (Anthropic's formalisation of Fermat, and Buzzard's assessment); provenance and paternity (Navier-Stokes, and the Borisov-Gabber-Vasiu precedent behind the Jacobian-conjecture counterexample); the cost of externalisation priced in position-years; the AHGT Taming the flow seminar; institution-hosted open-weight models; the standing-positions page. New footnotes in §§ 1.2.2, 2.1, 2.2, 2.3, 3.3.

• 2026.08.29 Publication. ArXiv submitted (26 pages, 3 figures, 2 tables)

• 2026.08.28 Version 2. New section on students and teaching; the loop kept whole as a new practice; the retreat to aesthetics declined [Avi25]; the overhang of [Bes26]; the unit to fund as a new type of structure; the provision of the corpus as a common-pool resource, and polycentricity as the form the new structures take [Ost10]; declared scope on political economy and access; position with respect to [KT26]; new sources: the 2024-2026 literature, K. Ono (20 July 2026), Aumann on 'same priors'; ArXiv update (26 pages; 3 figures, 2 tables).

• 2026.08.13 Publication. Bloomberg published [Ols26]; ArXiv submitted (17 pages, 2 figures, 2 tables);

• 2026.08.05 Minor Additions. The investigation on non-sofic groups, Figure 2;

• 2026.08.01 Version 1.