Methods

Mark Pesce · University of Sydney · August 2026

Abstract

The methods section is the part of a scientific paper that lets a stranger attempt what its authors did: do this, and you should see what we saw. The newest results in mathematics have no methods section. A counterexample that ended an eighty-seven-year-old conjecture was drawn from the latent space of a language model - the published record holds the object and its certificate, and no path at all - certified afterwards by a proof kernel that was never inside the discovery. The result is certified; the method is missing. This paper argues that the condition is general: post-Watershed, discovery becomes oracular while verification becomes mechanical, and the scientific method reconstitutes as a translation protocol between the two languages identified in the previous paper - forcing whispers from the latent space into the formal channel, or discarding them. The structure is old. Ramanujan and Hardy ran it by hand; Poincaré described its mechanism in 1908. What is new is that the generator scales as far as compute allows and the discriminator at the bottom of the loop has no discretion to corrupt - which matters, because the auditor always could be bribed, and the reproducibility crisis was science discovering that about itself. Vulnerability is not eliminated by the closed loop; it is conserved, and migrates upstream, coming to rest in the question. What replaces the methods section is the record.

1. The Letter from Madras

Late in January 1913, G. H. Hardy, then the most exacting pure mathematician in England, received a package from Madras, its covering letter dated the sixteenth. Inside were nine pages of mathematics from an accounts clerk at the Madras Port Trust earning twenty pounds a year: roughly one hundred and twenty theorems, stated bare, without proof, without derivation, without apparatus of any kind.[1] Some Hardy recognised. Some he knew to be wrong. And of some he later wrote: 'They must be true because, if they were not true, no one would have had the imagination to invent them.'[2] He spent that evening with Littlewood working through the pages, and by midnight the two had concluded that the unknown clerk was a mathematician of the first rank - a verdict reached entirely from outputs, because outputs were all there were.

Srinivasa Ramanujan had formed himself above all on one book - Carr's Synopsis of Elementary Results in Pure and Applied Mathematics, a cram-school compendium of some five thousand theorems stated, in the main, without proof - with a handful of others, Loney's Plane Trigonometry among them, beside it.[3] From that compressed corpus he had somehow internalised the deep structure of the discipline, and what he produced from it was structure without derivation: identities, series, continued fractions, arriving whole. Asked for his method, he named a goddess. The theorems of his family deity Namagiri, he said, unrolled before him in dreams; an equation had no meaning for him unless it expressed a thought of God.[4] Nor was the oracle infallible. His claims about the distribution of primes were wrong - subtly, instructively wrong, in ways that took the full machinery of complex analysis to diagnose.[2] What Hardy built in response was not a demand for methods. It was a harness: bring the generator to Cambridge, pair it with discriminators of the first class, test every claim against proof, publish what survived, record what failed. Hardy supplied rigour, proof, and real collaboration - the two published serious mathematics together - but above all he supplied judgment, and the institution that turned an oracle into mathematics.

Every element of the newest way of knowing is present in this hundred-year-old arrangement: a generator producing connections without derivations from a compressed corpus, an unverifiable account of its own workings, a false-positive rate, a discriminator wagering on accuracy he could not yet demonstrate, and an institution built to convert one into the other. What has changed is scale and substrate. The generator is now minted by the trillion, and the discriminator at the bottom of the loop is no longer a Fellow of Trinity but a proof kernel that cannot be flattered, tired, or paid.

This series has described the economics of collapsed-cost cognition,[5] the verification that converts unreliable cognition into trustworthy work,[6] and, most recently, the horizon past which outputs exceed every human judge, leaving a relative superintelligence two working languages: the formal, which is checkable and sealed, and the oracular, which is accurate and illegible.[7] This paper is about the machinery between those two languages. Section 2 locates the generator. Section 3 states the old mechanism of discovery it accelerates. Section 4 examines the auditor science has always relied upon, and the crisis that exposed him. Section 5 documents the closing of the loop in mathematics, the first science to fall. Section 6 addresses the section that has gone missing from the scientific paper, and what replaces it. Section 7 states a conservation law. Section 8 concludes.

2. The Space of Connections

A language model in training compresses the patterns of an enormous corpus into a high-dimensional internal representation - the latent space. Concepts that recur in similar relations draw near one another in that space even when they belong to distant disciplines, which gives the trained model a capacity nothing individual has ever had: it can surface candidate connections across more of the recorded surface of human knowledge than any person has read. Not deep connections, necessarily. Wide ones. The previous paper defined the discernment horizon vertically: the hardest answer you can judge.[7] There is a lateral counterpart. A proposed correlation between, say, a technique in algebraic number theory and a problem in discrete geometry may lie within the competence of experts on each side, while the conjunction lies within the view of no living person, because no one holds both contexts at once. Call this the 'breadth horizon'. The latent space does not see over the tallest expert. It sees across more of them than anyone.

The honest qualifications are structural, and they define everything that follows. The latent space is not a searchable map; its relations are distributed, not indexed. It learns association, not causation, so it will propose elegant connections that are elegantly spurious. Its coverage of rare expertise is thin precisely where expertise is rarest. And - this is the pivot on which the whole paper turns - its proposals arrive in the language of the oracle. A candidate connection surfaced from latent space typically arrives without a derivation its receiver can rely on: structure stated bare, exactly as the theorems arrived from Madras. When such a proposal is true, it is oracular in the strict sense of the previous paper - accurate, and illegible at receipt. When it is false, it can arrive looking identical. The uncomfortable centre of The Limits of Truth was that profundity and confident noise cannot be told apart from below.[7] The latent space produces both, fluently, at near-zero marginal cost.

So the correct description of the generator is neither the enthusiast's 'intelligence beyond experts' nor the sceptic's 'stochastic parrot'. It is a conjecture engine: a device for proposing relationships across a conceptual surface no single mind has surveyed, with no warranty attached to any individual proposal. On its own, such a device is useless or worse. Attached to the right loop, it is the most productive instrument in the history of inquiry. The difference is entirely in the loop.

3. Variation and Selection

In 1908, Henri Poincaré described the mechanism of mathematical discovery from the inside: a period of conscious work, then an incubation during which 'the subliminal self' combines ideas in vast numbers below awareness, and finally the surfacing of a few candidates selected - he was insistent on this - by an aesthetic sieve, the sterile combinations never presenting themselves at all.[8] Discovery, in Poincaré's account, is variation and selection: an abundant, undirected generator below, a severe discriminator above. Ramanujan and Hardy were the same architecture split across two people and an ocean. Although this loop is not new, the machinery of this decade has industrialised the halves separately. Generation has been minted; the subliminal self now runs on rented hardware at whatever scale the budget allows. Selection has been minted only in part: the mechanical test of validity, as Section 5 shows, automates completely, while the selection that judges what matters has not - and the entire economics of post-Watershed science follows from that asymmetry.

The productive arrangement is a division of labour. Models are broad, fast, indefatigable generators; they can propose the unconventional without embarrassment, because proposing costs next to nothing. Humans are contextual discriminators: they judge relevance, causal plausibility, significance, and whether an idea survives contact with a reality they have embodied experience of. Experiments are the final arbiters. The workflow is therefore not ask the oracle for the answer. It is: generate widely; require the proposed mechanism, its assumptions, and its falsification tests alongside every candidate; rank; let experts attack the survivors; test what remains. The workflow is older than it looks: in Herodotus's telling, Croesus ran it at Sardis - seven candidate oracles, one falsification test whose answer did not yet exist when the messengers left, the field cheaply winnowed, the survivors promoted - and the previous paper records what it cost him to stop there.[7] Run this way, an extravagant false-positive rate is not a defect but a budget line. A generator that yields a hundred strange hypotheses is a bargain if qualified discrimination can cheaply reject ninety-nine, because the hundredth opens a line of inquiry no one would have walked to - and Foundations already named the economics: the tokens are the cheap input, and the alpha is in what the tokens cannot mint.[5] What the tokens cannot mint here is the sieve. The binding constraint of science has inverted where the loop has closed: conjecture there is abundant, and judgment is the bottleneck - and judgment, Foundations observed, travels under an older name. Hardy's contribution to the collaboration was not theorems. It was taste: knowing which of the nine pages mattered. Taste is the non-mintable residue of the scientific method, and it has just become the most valuable element of the human share.

4. The Bribable Auditor

Humans are great discriminators. Great is not perfect, and the imperfection is not primarily cognitive. Discrimination is never independent of incentives, and the auditor can always be bribed - literally on occasion, but far more often institutionally, ideologically, or through the ordinary career pressures of a profession that pays for novelty, publishes positives, and promotes on volume. Peer review - with roots in the seventeenth century, spreading through the nineteenth, standardised only in the twentieth - sits low on the ladder of judges: a proxy, corruptible in every way the earlier papers catalogued.[6] Reviewers tire, favour their schools, defer to eminence, and normally do not rerun the experiment.

Science discovered this about itself, painfully and in public, in the decade before the Watershed. In 2005 John Ioannidis modelled the conditions under which most claimed research findings would be false, and argued that those conditions commonly obtain;[9] in 2015 the Open Science Collaboration attempted to replicate one hundred published psychology studies, and by the conventional significance criterion roughly a third replicated - between a third and a half, across the project's several criteria.[10] The reproducibility crisis is conventionally told as a story about statistics. Told in the vocabulary of this series, it is in large part a Goodhart event - not the whole of it, for low power, error, and honest fragility all contribute, but the incentive core: publication became the target, so publication ceased to be a measure. P-hacking is reward hacking by researchers, deliberate or not; the significance threshold was a benchmark, and it was gamed; the literature is what a corpus looks like after decades of optimisation against a corruptible judge. Evaluating Intelligence described the collapse of the instruments that measure machine minds.[11] The instruments that measure scientific claims collapsed first, for the same structural reasons, and the profession has spent twenty years attempting to reform the auditor - preregistration, registered reports, open data - which is to say, attempting to make the bribe harder to pay. Harder is not impossible. It never is, while the judge has discretion.

Then the enterprise met, in its own house, a judge with no discretion at all. A proof kernel is a deliberately small program - small enough to be audited end to end - that reads no reputations, holds no school, needs no grant, and rules only on whether each step follows.[6] Within its reach it is a referee that cannot be bribed, because there is no discretion to buy. Its guarantee is conditional - on the statement encoded, the axioms admitted, the small trusted base - and those conditions are exactly where Section 7 sends the risk. The sciences within its reach noticed immediately.

5. The Loop Closes

The unit that does modern discovery is not a model. It is a loop: model, tools, data, feedback, permissions, and human collaborators, arranged so that every candidate the generator surfaces is driven toward a verdict. In mathematics the loop closed first, and Defending the Loop explains why it had to: automation proceeds along the gradient of verifiability, and mathematics already possessed the incorruptible judge.[6] Conjecture, formalise, attempt, and the kernel rejects with an exact complaint; the complaint steers the next attempt; no human sits inside the cycle. The rejection is not merely quality control - it is a teaching signal that never lies about validity within its formal boundary, which is why capability against it compounds; what the signal does not vouch for - significance, intent, the worth of the target - Section 7 takes up.

The confirmations arrived within months of each other, and they climb. In June 2026, an agentic system working against continuous inference-time feedback from the Lean checker solved all twelve problems of the 2025 Putnam competition and lifted a general model's formal solve rate on competition benchmarks from under ten per cent to seventy.[12] In May 2026, an OpenAI model refuted Erdős's unit-distance conjecture, standing since 1946, by importing machinery from algebraic number theory that the assessing mathematicians judged new and effective in that setting - a breadth-horizon crossing, executed at depth; the announcement was checked by human mathematicians in May, and the Lean formalisation closed the loop on 26 June.[13] DeepMind's Aletheia system - generator, verifier, reviser, restart - has produced contributions to open problems that its own builders carefully decline to call landmarks, which is itself a sign of health: actual research, modestly claimed - its verifier a natural-language critic, its grading human, a loop still running below the kernel.[14]

Then, on 20 July 2026, Levent Alpöge announced a counterexample to the Jacobian conjecture, posed by Ott-Heinrich Keller in 1939 and listed by Smale among the problems for this century: an explicit polynomial map from ℂ³ to ℂ³, credited to Claude Fable, whose Jacobian determinant is identically −2 and which nonetheless sends three distinct rational points to a single image. The map is therefore not injective and can have no polynomial inverse; the conjecture fails in dimension three, and, by adjoining identity coordinates, in every higher dimension. The two-dimensional case stands open.[15] The result was independently formalised in Isabelle/HOL: the kernel checked the derivatives, the constant determinant, the collision of the points, the impossibility of the inverse, and the extension upward. Note what this artefact is. Unlike a long prose proof, the counterexample has an almost perfectly hard surface: either the determinant expands to −2 and the listed points collide, or they do not. The auditor was left no discretionary space in which a bribe could even be tendered. And note, equally, what the kernel did not do: it was never inside the discovery. The object came out of the latent space of a language model, and the public record contains no path: no prompt, no parameters, no trajectory a stranger could inspect or rerun. The formal loop closed around it afterwards, converting an intriguing claim into certified mathematics. Discovery oracular; verification mechanical; the method, in between, is the part that made the second possible for the first.

Nine days later it happened again, one domain down the ladder. On 29 July 2026, three mathematicians published a counterexample to the Maxwell conjecture, a bound on the equilibria of point charges read out of Maxwell's 1873 Treatise on Electricity and Magnetism and stated precisely in 2007: five charges whose potential admits at least twenty-four non-degenerate critical points, where the bound allowed sixteen.[16] The idea for the construction was suggested by a language model - OpenAI's GPT-5.6 Sol - and the authors verified the mathematics, wrote the argument in their own words, and checked the computations with computer algebra: a judge below the kernel, and the strongest the object has yet faced. The paper carries a section still new to the genre, a 'tool and computational resource disclosure', naming the generator and describing the checking - provenance, in embryo, beginning to stand where the methods section stood.

One disclosure, in the register this series has already established. The system credited with the counterexample is kin to the system assisting with this paper, and the reader should weigh that exactly as the previous paper instructs: testimony from the source is inadmissible, and no mathematical weight in this argument rests on it.[7] That weight rests on a kernel that has no kin. The claims of provenance rest, as provenance always does, on the disclosures and records of those involved - which is the next section's subject.

6. The Missing Section

When the Royal Society constituted modern science in 1660 and, in its First Charter of 1662, took as its motto nullius in verba - take nobody's word for it[17] - the instrument of that refusal was the reporting of method: in embryo in the witnessed demonstration and the experimental letter, in canon by the twentieth century's standardised Methods section. The rule beneath the changing forms never changed: a result and the path to it travel together, so that trust attaches to the path and not to the person. That is where science has kept its provenance.

The Jacobian counterexample has no methods section, and cannot have one. The discovery was a sample from a model's distribution, and what has been published is the object and its certificate: no prompt, no parameters, no trajectory - no protocol a stranger can repeat. Whatever fuller record may exist, nothing public lets anyone inspect or rerun the path; asked for the method, the record answers as Namagiri did. The result is machine-checked end to end, recheckable by anyone, forever - and its provenance is a whisper. Post-Watershed science decouples the result from its method: keeps the certificate, loses the path. The section the scientific paper was built around is empty - which is why this paper bears its name.

What replaces it is the answer this series keeps arriving at from every direction: the record. Where an artefact can carry its own proof, the certificate answers the one question the methods section existed to answer about correctness - and answers it, for that question, with a stronger warrant than a stranger's replication.[6] What it cannot answer - where the claim came from, whether the formal statement is the intended one, how the discovery behaved - is exactly what a record must still carry. Nullius in verba, aspired to for three hundred and sixty-four years, is achieved literally in that one dimension: nobody's word is taken, not even the discoverer's, not even the checker's colleagues' - only the checker's, and the checker has no words, only verdicts. But provenance of the programme becomes more important than it has ever been, because the generator is an oracle, and oracles, the previous paper argued, can be relied upon rationally on exactly one basis: their ledger.[7] A conjecture engine has a hit rate. It has calibration, domains of strength, characteristic failure modes, a history of proposals and outcomes. That history - claim, check, outcome, attribution - is the verification record of discovery, and it does for the generator what the methods section did for the experiment: it tells you what your trust is standing on. The unit of science shifts accordingly. Not the paper, that bundle of claim, narrative, and unrepeatable path, but the certified claim travelling with its record - and the programme behind it, priced continuously on everything it has claimed before.

7. The Conservation of Vulnerability

A law has been operating unnamed through every paper in this series, and it should now be stated. Mechanising a layer of verification never eliminates the corruptible residue. It relocates it upstream. Ariane 501 moved the failure upstream, out of disloyal code - there was none - and into design decisions and premises inherited from a slower rocket.[6] Defending the Loop moved it from implementation, which the kernel polices, into specification, which no kernel can. This paper moves it once more: the kernel guarantees that a formal term proves the encoded statement under the encoded axioms. It cannot guarantee that the encoded statement is the one intended, that the axioms are apt, or that the theorem was worth anyone's while. The auditor cannot be bribed - so the bribe, such as it is, migrates to the author of the audit standard, and above the author of the standard stands the chooser of the question. At the top of the chain, vulnerability comes to rest in the act that automates last and least: deciding what is worth asking. Machines now propose questions too; what stays human is the assignment of value, risk, and resources to a question, because that is where accountability stays. Call it the conservation of vulnerability - offered, in honesty, as a design heuristic pressed into service as a law, exact nowhere, observed everywhere.

The law fixes the human station in post-Watershed science, and it is Hardy's station. Not generating: in the domains the loop has reached, the latent space out-generates humanity. Not checking: there, the kernel out-checks it. Directing and ratifying: choosing which questions are worth the loop's time, which premises to encode, which standards to demand, and reading the formalisation to confirm that the statement proved is the statement meant - the last duty, ratification, being exactly the one the previous paper showed drowning first past the discernment horizon.[7] The scientific taste that funded Ramanujan's passage to Cambridge becomes a profession, the successor to most of what was called research.

The station is under a pressure the law predicts, because the law applies with full force to this paper's own remedy. The ledger of Section 6 is a verification layer, and mechanising trust relocates the residue exactly as the law requires: upstream, into vigilance. The ledger prices the programme, never the claim - Ramanujan's ledger was as extraordinary as any on record the day his theory of primes failed, and it was proof, not provenance, that caught it - so the record can govern triage only, while acceptance belongs to the judge. That boundary will not hold by itself, because over-belief in a good ledger is not a failing; it is the equilibrium. Discrimination grows more expensive as the horizon rises; the record grows cheaper and better; substituting one for the other becomes the economically rational act at precisely the moment it becomes fatal. Cheap trust drives out expensive trust. The dynamic has a name in the automation literature, forty years old - Bainbridge's irony: the more reliable the machine, the worse the human monitor, vigilance atrophying as the reliability that makes it seem unnecessary grows.[18] The good-enough ledger is precisely the one nobody checks; the Watershed's own thesis casts this shadow. It is what the oldest institutions understood better than we yet do. Rome kept its Sibylline collections under guard for the better part of nine hundred years, and consultation still ran through decree, college, and deliberation before any rite was performed. The friction was not reverence. Ritual was a forcing function, the mechanism by which discrimination is kept non-optional when the record says relax. The rite was never for the god. It was to prevent the worshipper from trusting the god too cheaply.

The law also maps where the loop cannot yet close, which is a map of the near future of every science. The loop requires a judge, and judges vary. Mathematics had spent fifty years building its judge, and when the generators arrived it was taken in months. Code has the spec and the suite. Beyond them the ladder descends through the physical sciences, where the judge is nature read through an interpretation layer - and the interpretation layer, the A-Lab affair demonstrated, is corruptible in exactly the old way, automated confidence standing in for human reading until human crystallographers reread it.[6] Below that, the sciences of complex and reflexive systems, where the judge is statistical, slow, and Goodhartable, and where the reproducibility crisis lives. The sciences will fall to the closed loop in order of the quality of their judges - not in order of their prestige, their funding, or their proximity to application. The gradient of verifiability is the timetable.

8. Conclusion

Two documents stand at the head of the scientific method. Descartes' Discourse on the Method built it for a single reasoner, and its first rule - accept nothing as true that is not clearly known to be so - has waited four centuries for an executor with the patience to apply it literally.[19] Bacon's Great Instauration built it for an institution, and stated the aspiration with a precision that has become uncomfortable: the mind 'not left to take its own course, but guided at every step; and the business done as if by machinery.'[20] Bacon's phrase was a metaphor for method. It is no longer a metaphor. The business is done by machinery - and the arrangement that has emerged would have startled both men: a generator that cannot show its work, a checker that cannot want anything, and between them, holding the ledger, the only party in the loop with something at stake.

The framework predicts the following. The sciences fall in order of judge quality. Mathematics has fallen; code is falling; each discipline joins the loop economy roughly when its verification can be made incorruptible enough - enough meaning that cheating the judge costs more than satisfying it, a line that moves as the loops grow stronger. Judge-building is therefore a maintenance discipline, not a milestone, and it will be the great scientific investment of the coming decade: assay automation, interpretation layers hardened against their own fluency, formal specification of what a positive result is, rebuilt as often as the loops require. The paper dies as the unit of science. Its successor is the certified claim travelling with its record; journals either become registries of records or become ceremonial. Peer review migrates upstream. Refereeing results is the kernel's job now, wherever the kernel reaches; the reviewers' discretion relocates to premises, standards, and significance - auditing the audit standards, in the appellate role the conservation law predicts. Discovery programmes are priced like oracles. Funders, and in time insurers, underwrite generators on their ledgers - hit rates, calibration, the record of claims and outcomes - and the uninsurable programme goes unfunded, which becomes the operational meaning of pseudoscience. And the reproducibility crisis ends by bypass, not by reform. The corrigible sciences will not fix the old auditor; they will route around him, as certified machine claims outcompete irreproducible human ones - gradually, and then suddenly.

The framework does not predict timing, and it does not predict reach: whether the loop's judges can be built for the sciences of minds and societies, or whether those fields remain oracular indefinitely, is exactly the kind of question the framework says cannot be answered from below. It makes no claims about what the generator understands; nothing in this paper requires the latent space to be a mind, only a surface no single mind that reads it has read the whole of. And it leaves one small conjecture of its own, offered in the spirit of the letter from Madras. The two-dimensional Jacobian case is still open. Somewhere in a latent space, plausibly, so is its answer - stated bare, without derivation, waiting for a discriminator with the taste to ask.

Acknowledgements

This paper was inspired in part by Kevin Kelly's essay "Latent Space as a New Medium"; as they have for more than thirty years, his thoughts inspire my own. Profound thanks to John Allsopp, Jessica Simon and Alan Eyzaguirre for conversations that shaped this argument, and to Philippe van Nedervelde for his continuing encouragement. This paper was composed with the assistance of Claude Fable 5, under the disclosure recorded in Section 5. I remain wholly responsible for any errors that may have crept in.

Notes

1. The letter, dated 16 January 1913, and Hardy's response are reproduced in Robert Kanigel, The Man Who Knew Infinity: A Life of the Genius Ramanujan (New York: Scribner, 1991).
2. G. H. Hardy, "The Indian Mathematician Ramanujan," The American Mathematical Monthly 44, no. 3 (1937): 137-155. The judgment quoted - 'they must be true because, if they were not true, no one would have had the imagination to invent them' - appears there, as does Hardy's assessment that Ramanujan's theory of primes was vitiated by his ignorance of the theory of functions of a complex variable.
3. George Shoobridge Carr, A Synopsis of Elementary Results in Pure and Applied Mathematics (London, 1880-1886): approximately five thousand results, stated in the main without proof.
4. Kanigel, The Man Who Knew Infinity, on Namagiri and on Ramanujan's remark that an equation had no meaning for him unless it expressed a thought of God.
5. Mark Pesce, "Foundations of Post-Watershed Economics," The Watershed, April 2026. https://thewatershed.markpesce.com/foundations-of-post-watershed-economics/
6. Mark Pesce, "Defending the Loop: Verification and the Division of Labour in Autonomous Work," The Watershed, July 2026. https://thewatershed.markpesce.com/defending-the-loop-verification-and-the-division-of-labour-in-autonomous-work/
7. Mark Pesce, "The Limits of Truth: Verification in Relatively Superintelligent Systems," The Watershed, July 2026. https://thewatershed.markpesce.com/limits-of-truth-verification-in-relatively-superintelligent-systems/
8. Henri Poincaré, "L'invention mathématique," in Science et méthode (Paris: Flammarion, 1908); in English as "Mathematical Creation."
9. John P. A. Ioannidis, "Why Most Published Research Findings Are False," PLoS Medicine 2, no. 8 (2005): e124.
10. Open Science Collaboration, "Estimating the reproducibility of psychological science," Science 349, no. 6251 (2015): aac4716.
11. Mark Pesce, "Evaluating Intelligence," The Watershed, June 2026. https://thewatershed.markpesce.com/evaluating-intelligence/
12. LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks (2026), an agentic framework using continuous inference-time interaction with the Lean compiler: twelve of twelve on the 2025 Putnam; Lean-IMO-Bench solve rate raised from under 10% to 70%; and a machine-verified proof of a research-level combinatorial subproblem. https://arxiv.org/abs/2606.03303
13. OpenAI, Planar Point Sets with Many Unit Distances (May 2026), refuting the conjecture of P. Erdős, "On sets of distances of n points," American Mathematical Monthly 53 (1946): 248-250; independent mathematical assessment at https://arxiv.org/abs/2605.20695. The result was checked by human mathematicians after its announcement; the Lean formalisation was completed by a coding agent with a human on the loop on 26 June 2026: https://lean-lang.org/eval/problems/erdos_unit_distance_conjecture_false/
14. Google DeepMind, "Accelerating mathematical and scientific discovery with Gemini Deep Think" - the Aletheia loop: generator, verifier, reviser, restart. https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/
15. Ott-Heinrich Keller, "Ganze Cremona-Transformationen," Monatshefte für Mathematik und Physik 47 (1939): 299-306; Steve Smale, "Mathematical Problems for the Next Century," The Mathematical Intelligencer 20, no. 2 (1998): 7-15, Problem 16. The counterexample, announced by Levent Alpöge on 20 July 2026 and credited to Claude Fable, with its Isabelle/HOL formalisation: https://isa-afp.org/entries/Jacobian_Counterexample.html
16. Philip Arathoon, Gavin Ball and Matthew D. Kvalheim, "The Maxwell Conjecture is False," arXiv:2607.27197, 29 July 2026. The conjecture derives from J. C. Maxwell, A Treatise on Electricity and Magnetism (1873), §113, and was stated precisely by A. Gabrielov, D. Novikov and B. Shapiro in 2007. The paper's disclosure reads: 'The idea behind this construction was suggested by an LLM (OpenAI's GPT-5.6 Sol). The authors have verified the mathematical details and have written the argument in their own words.'
17. The Royal Society, founded 1660; the motto nullius in verba was adopted in its First Charter, 1662; after Horace, Epistles I.1: 'nullius addictus iurare in verba magistri.'
18. Lisanne Bainbridge, "Ironies of Automation," Automatica 19, no. 6 (1983): 775-779.
19. René Descartes, Discours de la méthode (Leiden, 1637), Part II, first precept.
20. Francis Bacon, The Great Instauration (1620), "The Plan of the Work," in the Spedding translation: '...the mind itself be from the very outset not left to take its own course, but guided at every step; and the business be done as if by machinery.'