Benjamin Collas, Mathematics Researcher

Topic 1 · Kyoto, 12 September 2026 · #permalink

The residue is now free. The product was never priced — and the same machines could shorten the climb

A field that has always ingested new tools Essay, §1.1

Absorbing a new mode of production is ordinary work here. What is new is that the means of production belong to someone else.

• We did it with computer algebra in the 1990s, and we have been doing it since about 2020 with mass collaboration and with formalisation.
• The field is moving fast, and in public: two special issues of the Bulletin of the AMS in 2024, the Leiden Declaration drawn up in under a year, a public lecture at ICM 2026, dedicated funding structures. A field that changes on the scale of two generations has reorganised its conversation in a semester.
• What is not ordinary this time is that the means of production belong to someone else. That single fact turns a question about tools into a question about institutions.

What is produced now Essay, §1.2

Machines produce the countable half, and produce it well. They do not choose what is worth naming.

• Two kinds of result. First counterexamples, which prune a branch that grew the wrong way. Then solutions to open problems. Both are real; neither is the whole of the work.
• The other half is choosing: which definitions are worth making, which objects deserve names. No system performs that choosing today. A theorem is only as good as the notions it is stated in.
• $2,000 does not buy a theorem. It prices one success, not the search that found it, nor the failures, nor the model behind it. What it buys 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.
• Capability rests on context. A year ago these systems behaved like badly educated students; they are now well trained, and can tell a poor direction from a promising one. But the contribution stays narrow, and it rests on context already built: the definitions, the libraries, the accumulated understanding — the connections standing unnoticed in a literature nobody can read, the overhang in David Bessis’s word. Harvesting a corpus is not producing one.
• And if machines do come to choose the notions? The concession costs the argument nothing. What changes is who chooses, not that choosing is the scarce act: someone must still recognise a good choice as good, and that is settled downstream, by what can be built on it. It is the judgment, not the generating, that is at issue.

What was always the product Essay, §1.3.1

A theorem transmits a capacity to think; that capacity has to be rebuilt in every reader.

• The writing, the seminar, the refereeing are that rebuilding, and none of it is what the theorem states.
• The residue also orients. A conjecture is the negative imprint of many residues — countable, publishable, not even proved — and its whole office is to make a horizon visible, so that someone knows where to look next.
• We are funded as if theorems were the product, and we sell teaching as the justification. Both are residue.
• One retreat to decline. Jeremy Avigad names the temptation: threatened by the economic argument, mathematicians may fall back on aesthetics — we do this because we enjoy it, as one enjoys literature or art. The claim here is not that mathematics is a pleasure society should indulge. It is that this is the one such practice that can check a trillion-dollar industry’s claims without that industry’s permission (see topic 2). Classical music cannot audit anyone.

The bluff, called Essay, §1.3.2–§1.3.3

The economics were wrong before the machines arrived. Falling costs simply made the scarce half visible.

• AI did not create this problem. It called a bluff long on the books, by driving the cost of the residue towards zero.
• The bluff was on public record. In 2019 Japan’s ministries published The Coming Era of Mathematical Capitalism, naming the country’s top three science priorities as “mathematics, mathematics, and mathematics”, and asking — without answering — what social system would suit such an era. The membrane between what we understand and the economy is now permeable in both directions: the traffic is priced.
• 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. None of those studies prices what the essay calls the product.
• An externality, in the ordinary sense. Responsibility for correctness is the cheap half, and it is now machine-dischargeable. The expensive half — reading, situating, repairing, teaching — is left to us, and takes years.

What the same machines could make Essay, §3.3.2, Coda

Turned outward, the same tools shorten the climb to the frontier instead of raising the volume to be absorbed.

• They lower the cost of entering a field: expertise becomes something a newcomer builds, rather than a barrier already cleared.
• There is a real acceleration available, it is just not the one being sold. Compressing the countable stages does not accelerate understanding (see Thurston’s foliation experience, with no AI). What AI can shorten is each participant’s climb to the point of being able to take part — absorptive capacity, in the economists’ word. What it cannot shorten is the deliberation by which a result becomes standard.
• A new instrument makes a new way of working before it makes a new result. Reading and writing had long been dissociated acts, separated by months; the tool brings them into contact, so that one questions while reading and tests while writing.
• A division of kinds, not a division of labour: randomness from the language models, rigidity from the Lean kernel, judgment from people — each supplying what the other two cannot.
• None of it is automatic. It holds where the practice is built for it, and where the tools stay open enough to be turned back on the material — questioned, replayed, explained. Anchored in academia, it opens a wider door. Left to access granted by AI labs case by case, it is a gate.

Topic 2 · Kyoto, 12 September 2026 · #permalink

A result with no author: what is missing is not a rule, but an anchor in academia

A trillion dollars rests on a certification that is ours Essay, §1.2.2, §1.3.3, §2.3.1

No scientific confirmation, no capability claim; no capability claim, no valuation.

• The industry’s valuations rest on claims about what its systems can do, and almost all of those claims are certified by the party making them. That is a measurement problem the public cannot solve on its own: whoever has the financial incentive to optimise the score is also the party producing it.
• Goodhart’s law, and here not a metaphor. When a measure becomes a target it ceases to be a good measure — and in this case the measure is itself the product being sold.
• A capability claim is worth what its certification is worth, and the certification is ours. It is designed, run and refereed by the community. Ten solved problems become evidence about a system only if people qualified to judge say so, and that evidence holds only while the community certifying it still functions.
• So the dependency runs the other way. This is not a case for funding mathematics; it is a description of what the valuation rests on. An audit capacity that nobody maintains is an audit capacity that stops existing. Classical music cannot audit anyone.
• This is not a guild declaring itself indispensable. It is the ordinary requirement of any science: that a measure be certified independently of the party it measures.

What we can check, and what we cannot Essay, §2.1

A proof answers to no one’s permission. Whether a statement says what was meant answers to no kernel.

• Every other field that wants to check an AI company’s claims must ask that company for access, and access can be withdrawn quietly. We do not have to ask. No API key, no compute parity, no permission. The reason is technical, not virtuous.
• Formalisation is what makes this scale. It is the one form of refereeing that keeps pace with machine output, and it makes hallucination detectable — at the level of the proof.
• And it stops there. No kernel can check that a formal statement says what the mathematics meant. When one system writes both the statement and the proof, the verification establishes internal consistency: a ground for suspicion, not for reassurance.
• Our asset is also their raw material. The property that lets us audit them — a proof checkable with no human in the loop — is exactly what makes formalised mathematics ideal training material.

Three failures, one cause Essay, §2.1.3, §2.2

Scooping, missing paternity, and claims beyond one’s understanding are three names for one absence: nobody stands behind the result.

• Scooping. The rumour that someone is working on a problem is now enough to trigger a sweep of it. The incentive becomes to stop sharing directions, which would reverse centuries of open science.
• Paternity. We do not cite in order to pay people. We cite as lighthouses: a reference marks where understanding advanced, and tells a reader where to look next. An output with no lighthouses flattens the landscape, and a landscape without relief offers no journey.
• Claiming beyond one’s understanding. Claim a theorem only when the full details can be given. Claim authorship only for what one can explain.

Hence four questions, to put to any announcement, whoever makes it — a company or a colleague.

1. Is the complete argument public — the understanding, not only the residue?
2. Who chose the problem, and the terms in which it is stated — and when?
3. What independent checking process has been applied?
4. Who closes the loop — is there a named interlocutor, and terms under which the field can read, question, attribute, and build on the result?

None of this is invented for the occasion. The EMS Code of Practice already binds mathematicians to the first and the third; the Leiden Declaration asks industry to meet, at minimum, the standards we expect of our colleagues. We are asking no one for more than we ask of ourselves. And the third question already has an institution: First Proof, academic-led, ran a controlled evaluation of research-level problems refereed by the people qualified to judge it. The score is not the interesting output. Who designed and ran it is.

The structures are the story Essay, §2.3

What is being settled now is not the next result. It is the institutions, and the access, that outlast it.

• The two sides are not symmetric, and it cuts both ways. Two things sit on our side of the table and not on theirs: the evaluation, and the corpus. Each side is short of exactly what the other holds. That is a negotiating position.
• Access is not a neutral gift. One laboratory offers free access at scale, to a hundred thousand scientists; another opens its most advanced tools to five partner institutions. Both are granted, and both can be withdrawn quietly, without anyone breaching anything — only now with many people downstream of the decision. Free access at scale is dependency at scale, not a research partnership.
• A third kind of structure is emerging — neither corporate laboratory nor university department. It hires researchers and doctoral students, and builds interfaces; what it needs from academia is recognition, funding and partnership.
• The form is not the practice. Such a structure can produce work a field can build on, or volume the field must then clean up. Which of the two depends on the anchor: representatives of academia with the standing to say what would count as usable, and answerable for having said it. The anchor is academic because academia is the one party whose output is science for everyone — published, taught, and usable by people who were never in the room. What keeps such a structure an interface rather than a gate is what leaves it: open code, open publications, open access to the tools.
• The unit to fund is the structure, not the project. Projects and individuals are countable, which is precisely why they are the ones we fund.
• Complexity is not the same as chaos. A dozen overlapping institutes look like disorder, and the funding reflex is to merge them into a single national programme. Ostrom’s evidence says otherwise: many autonomous producers alongside a few shared services is no less efficient, and the best producers were more productive where many coexisted. These instruments are complementary to the ones we have, not rivals to them.
• Sovereignty, as much as economics. A country that stops training the people who can read and integrate what the machines produce has outsourced rather more than its compute.

One boundary, to avoid a misreading. These structures are for the crossing, where academia and the companies meet. They are not a new authority over what may be worked on. We need no new rules here: the code and the shared culture already bind us.

Topic 3 · Kyoto, 12 September 2026 · #permalink

The loop is the profession: what runs out is not problems, but the people who digest them and close the loop

The loop is the profession Essay, §3.1

Understanding tells us where to look; looking is what produces understanding. The loop holds for a person and for a laboratory alike.

• Understanding tells us where to look. Looking produces the residue. Reading that residue back is what rebuilds the understanding. Machines are strong over one quarter of that circle, and absent from the quarter that feeds it.
• Cut it, and the damage arrives at both ends at once — checking and cleaning up at the output, labelling and weighting at the input. A fear one hears is that the profession survives as a taste-labelling layer. Severed from practice, such a layer does not degrade: it never forms.
• Kept whole, the loop points the other way. A student can test an intuition in an afternoon where it used to cost months, and so can an established researcher working 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.
• It works at both levels, the person and the 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 next generation, and the routing Essay, §3.2

The danger is not the tool but the routing — and a career built on one arc of the loop is the same cut, institutionalised.

• Two countable ends. The AI labs have names for them: pre-training and post-training. A mathematics student appears at both — as a source in the first, as a corrector in the second, and as a mathematician in neither. Those ends are easy to fund, and they train no judgment.
• Here we disagree with Klowden and Tao. They envisage “an increasing division of labor” in mathematical research, in which one specialises in a few aspects of the process — directing AI assistants to prove results for a senior colleague, or mining the literature to propose directions. Specialisation at each side of the loop is the loop cut at both ends, and made into a career structure. That is a design for a department, and it is the wrong one.
• What to do instead. Classical training first and all along — definitions made by hand, proofs written out, the long slow reading; with weekly oral sessions following the traditional ``colle'' sessions. Then contact with the machine, early and supervised, in three stages: first the corpus, learning to read at a scale no one could read before; then the acceleration of experience, learning cheaply that a question was wrong; then investigation, the student’s own question, with the machine inside the loop rather than at its ends. The order is not decorative.
• We have run this experiment once. Computer algebra in the 1990s could have collapsed into a toolbox of computations, or into pure logic. What it produced instead was experimental mathematics, and a generation that thinks with machines rather than through them.
• 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 in the new structures, and what is experimented there will percolate back into academia. That is how a practice becomes a formation.

What actually runs out Essay, §1.3.3, §3.3

The corpus is non-rival; its provision is not. What depletes is expert attention.

• The corpus 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, drawn on a finite pool of expert attention from which nobody can be excluded. Elinor Ostrom named that kind of good, and showed that it survives when its users govern it.
• Compression is not acceleration. AI compresses the stages that can be counted, from an open problem to an argument on the page, and leaves untouched the stage in which a result is read, situated, exposed and taught — in the formal case, what Alex Kontorovich calls canonisation: reworking a verified development into library mathematics others can build on. It widens the distance between what exists and what is understood.
• Absorptive capacity is the missing quantity: the ability to use knowledge produced elsewhere, built only by doing research oneself. Free access to results confers little on a community that has stopped producing the people who can read them. Properly grounded, AI can raise that capacity — that is the acceleration worth having, and not the one being counted.
• 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 paying to speed up.

Nothing is lost Essay, §3.4, Coda

Priority gets noisier. The journey is untouched — and it is the thing that can be defunded.

• Split “discovery” in two. One sense is priority, first place in the ledger; machines will make that scarcer and noisier. The other is the journey, the passage from confusion to understanding, and it is indexed to a person, not to the ledger.
• The residue was always reproducible; the journey never was. Almost everything one will ever understand was discovered by someone else, and that has never once made the understanding less one’s own.
• It cannot be mass-produced, but it can be routed away — defunded, traded for what can be counted. That decision is ours, and it shows itself in budget lines and in the positions offered to people starting out.
• A virtuous loop is available: randomness from the models, rigidity from the kernel, judgment from people. Turned outward, the same tools lower the cost of entering a field instead of raising the volume it must absorb. The answer to Thurston's experience.