I thought the above was my question - just how good have the models (with harness) become? In fact, whilst it is obvious the models + harnesses are now rather good, harder questions have come to light. The rest of this article was my way of understanding the issues at hand better. An understanding on how things have changed from this:
To meeting these gaps (from the Leiden Declaration): Thirteen months ago I mapped AI’s contributions to physics and mathematics onto a spectrum running from rediscovery through synthesis to genuine discovery. Since then a still-training model has spent four days on a Millennium Prize problem, a 1939 conjecture has fallen to a single social-media post, and twenty-five Fields Medallists have signed a protest. The spectrum needs re-scoring. Here is the update, from first principles, with the combinatorics that explain why it went the way it did.
Part I and II linked here:
1. The four days #
On 1 September 2026, OpenAI heard a rumour or “found out” (it really doesn’t matter)….
Researchers at the company had picked up talk that two Millennium Prize problems were close to falling. They pointed a model still in training — one they describe as materially more capable than GPT-6 Astra — at what was left. Roughly ten thousand agents ran in parallel. Intermediate findings were consolidated and pushed back into the groups, and agents were reallocated as directions (or proofs), paid off or died. Eighty-eight hours later, on 5 September, the run produced a proof. Formalising it in Lean took another seventeen. OpenAI’s Mark Chen put the compute bill in the millions of dollars.
On 8 September the company published a 166-page manuscript and a public Lean repository. Within twelve hours the story had stopped being about mathematics.
Tristan Buckmaster of NYU had posted first. He and Levent Alpöge, a mathematician employed by Anthropic, had spent roughly a year on closely related fluid dynamics, using Claude and Codex under their own direction. On 15 August they proved finite-time blowup under smooth forcing for three model equations; on 22 August a Lean check cleared the Euler case. Buckmaster’s statement alleged that their unpublished direction had reached OpenAI days before the announcement, that he had been pressed over authorship, and that Alpöge had been pushed off a proposed write-up because of his employer. He reported being asked, per Axios’s account of the exchange, “Why would you ruin your career?”
Sébastien Bubeck, who ran the OpenAI effort and who a year ago was the loudest voice arguing that these models produce real mathematics, denied the substance. He apologised for the wording of that remark and says he withdrew it immediately. Sam Altman backed him. OpenAI stated that neither its researchers nor its agents saw the unpublished work, and that it did not access the pair’s data for this problem. It also conceded that it cannot entirely exclude the possibility that de-identified usage data improved its models.
Three days later, twenty-five Fields Medallists signed a declaration saying the goals of the AI companies and the goals of mathematics are severely misaligned.
All of which buried the fact that two other results had landed in the same stretch, from a third lab, and that nobody has disputed either of them. I come back to those in section six, because they change the scoring.
Figure 1 · Every event on a true time axis. The first six span eleven months. The last seven span eight weeks.
2. The paper trail #
Strip the dispute out and the September result has an ordinary academic pedigree.
Diego Córdoba and Luis Martínez-Zoroa opened the direction in a preprint first submitted in October 2024: build a singularity by letting different spatial scales feed one another. The idea worked, but their forcing term was not smooth enough to satisfy Clay, and a step was missing. Alpöge and Buckmaster took the strategy over and closed both gaps in August 2026. OpenAI then ran the same route at Navier–Stokes with a compute budget no university can match.
Figure 2 · The lineage of the September result, and the one link in it that is contested.
Two of those three steps are uncontested, and both are human. The argument is (from my vantage point) entirely about the arrow between the second and the third. There is also a fourth group almost nobody noticed: Adarsh Ganeshram, Valentin Duruisseaux and Anima Anandkumar announced a candidate blowup profile for Euler on 7 September, found by a physics-informed neural network, with no forcing and no boundary at all. That is the harder version of the problem. Their own manuscript says the stability argument stays conditional until the constants are certified, and the dispute a day later buried it.
3. What was actually claimed #
The headlines said a Millennium problem had been solved. That is too coarse to be useful.
Charles Fefferman’s official problem statement offers four ways to win. Two of them, A and B, ask you to prove that a smooth fluid flow with no external force stays smooth forever — in open space, or in a repeating box. The other two, C and D, let you cheat in a very specific way: you may stir the fluid from outside, provided the stirring stays perfectly smooth and well-behaved, and you only have to exhibit one flow that breaks down in finite time. Clay wrote those doors into the rules deliberately. A single counterexample settles them.
OpenAI’s Theorem 1.1 goes through doors C and D. It constructs a flow that starts at rest, is driven by a smooth force compactly supported in space and time, and whose velocity becomes unbounded at a finite moment while its kinetic energy stays finite. Corollary 10.6 supplies the periodic version. The unforced question — the one most people mean when they say “Navier–Stokes” — remains open. Clay still lists the problem as unsolved, its rules require publication plus two years of scrutiny plus general acceptance, and OpenAI says it will not claim the money.
Figure 3 · The Millennium problem’s four alternatives, and which two the September claim addresses.
Keeping those distinctions straight matters more than it sounds, because they are exactly what gets lost in a headline. A summary that drops the word “forced” is describing a different theorem. So is one that drops “Euler.”
4. How you build a singularity? #
Strip away the 166 pages and the mechanism is a geometric series.
Start with a slow, smooth background flow that already solves the equation under a gentle force. Choose that background carefully, so that a fine ripple laid on top of it grows on its own — it feeds off the shear in the background the way a flag feeds off wind. Time the ripple so it stays vanishingly small for almost the whole interval and surges only at the end: large enough to sharpen the flow, small enough that the analysis still holds. Then treat the result as your new background, and add a finer, faster ripple on top of that.
Each round takes less time than the one before. Infinitely many rounds therefore fit inside a finite interval. Speed runs to infinity at the end of it. The stirring force never does, because each round’s correction to the force is engineered to be far smaller than its correction to the flow. Holding that gap open, round after round, while viscosity works to smooth everything out, is what consumed the page count.
Figure 4 · The Córdoba–Martínez-Zoroa cascade: speed runs away while the stirring force stays smooth.
Terence Tao published a summary of this on 7 September, before OpenAI’s release, after Buckmaster explained it to him over the phone. He called the Alpöge–Buckmaster work a remarkable achievement and said he saw no obvious obstacle to pushing the method all the way. He also made a point worth sitting with: solving these problems is “only a proxy goal for the primary goal of developing mathematical understanding and insight.”
The part the coverage skipped
Two Spanish mathematicians opened the direction; two more carried it from a rough forcing term to a fully smooth one. What the machines did — for both teams — was carry a known strategy through the estimates, localisations and constant-tracking that had stalled everyone. That is a real contribution. It is also a specific kind of contribution, and naming it correctly is the difference between a forecast and a fantasy.
5. The arithmetic nobody runs #
Ten thousand agents sounds decisive. Work out what it buys and it stops sounding that way.
Model a proof as a chain of choices. At each step some number of moves look plausible — call it five. Chain forty of those together and the space of candidate proofs is five to the fortieth, around ten to the twenty-eighth. A twenty-nine-digit number. Now divide by ten thousand agents, which is ten to the fourth. You are left with a twenty-five-digit number. Parallelism subtracts from the exponent, and the exponent is where all the difficulty lives.
Cut the chain from forty steps to six, though, and the space collapses to about ten thousand. That is what a good ansatz does, and it is why the Córdoba–Martínez-Zoroa strategy was worth more to this result than the compute budget was. One insight moved the exponent. The GPUs moved a coefficient.
Figure 5 · Search spaces measured in digits, and the stars-and-bars count behind the Jacobian counterexample.
The second lesson in that figure is the asymmetry between finding and checking. Levent Alpöge’s counterexample to the Jacobian conjecture — open since 1939, and demolished in dimension three and above on a Sunday in July — is a single three-variable polynomial map short enough to post on X. Counting how many maps it had to be picked out of is a first-year combinatorics exercise. Monomials of degree at most five in three variables: distribute five units among three variables plus a slack bin, which by stars and bars is C(8,3), or 56. Three coordinate functions gives 168 coefficients. Allow five small integer values each and the space holds roughly ten to the one hundred and seventeenth candidates.
Verifying one of them takes a determinant and a collision check. Seconds. Finding one took eighty-seven years.
That gap is the engine under every result in this article. Lean matters for the same reason: re-checking a finished 166-page proof is a single pass, while producing it was eighty-eight hours across ten thousand workers. Cheap verification is what makes expensive search economically rational, and it is why formalisation has gone from a hobbyist pursuit to load-bearing infrastructure in about eighteen months.
6. The results nobody is fighting about #
The dispute has crowded out the fact that September 2026 produced two other mathematical results, from a third lab, neither of which anyone has contested.
On 10 August, an unreleased Anthropic research model raised the proven lower bound for the fraction of Riemann zeta zeros lying on the critical line from 41.6 per cent to 67.2 per cent. The previous record had stood since 2020. It cost 31 million output tokens across two sessions, and roughly 650 earlier ideas went nowhere first. Two mathematicians at the company validated the argument, two outside experts examined it at short notice, and a Lean proof was published alongside. Anthropic says plainly that it does not expect the technique to lead to a proof of the hypothesis itself.
On 4 September, four days before the Navier–Stokes announcement, the same company published something stranger and arguably more consequential: a complete machine-checked proof of Fermat’s Last Theorem. Claude worked largely autonomously for eleven days, produced 13 million lines of Lean and 29,500 intermediate theorems, and closed the whole chain. The human input was occasional high-level steering. Kevin Buzzard, who leads the community formalisation project this work drew on, reviewed the result and said it proves the theorem “with no assumptions other than the axioms of mathematics.”
Why the Fermat result belongs in this article at all
It contains no new mathematics, and Anthropic says so explicitly: what is novel is the verification. Wiles finished the proof in 1995. The community expected formalising it to take years — the blueprint for the opening phase alone runs to 86 pages. It took eleven days. Set that against the Kepler conjecture, where twelve referees spent four years and settled for ninety-nine per cent certainty, and machine-checked certainty took sixteen years to arrive. The stage of the pipeline that used to be the slowest is now the fastest.
Two details matter. The first is that the Fermat proof was checked against Mathlib’s own statement of the theorem by a comparator, and uses only Lean’s three standard axioms. That is precisely the independent statement audit that OpenAI’s repository, four days later, did not have — its review status is marked self-assessed. The gate existed. One lab walked through it and the other did not.
The second is how it was done. The first attempts failed: agents lost track of the project state and stopped collaborating, and roughly seven per cent of the final lines were wasted effort. What fixed it was an external coordination layer holding a directed graph of theorem statements, separating statements from proofs, and giving each one a natural-language description so agents could find and reuse it. A memory architecture, in other words, rather than a better model. The same finding, from a different lab, on a different problem, in the same month.
And there is a sting. Thirteen million lines of Lean is about five times the size of Mathlib, the library the whole thing rests on, and Anthropic concedes the proof is probably far longer than it needs to be. No human will ever read it. The company is careful to say a formalised proof should not replace a human-readable exposition. So the result confirms Tao’s objection rather than answering it: correctness got cheap, and the distance between a proof being checkable and being teachable got wider.
7. Re-scoring the spectrum #
The 2025 framework plotted results on two axes: how novel the outcome was, and how much it leaned on human priors. Rediscovery sat in one corner, synthesis in the middle, genuine discovery in the far reaches nobody had reached. Plotting the last thirteen months on the same axes produces a clean and slightly uncomfortable picture.
Figure 6 · Thirteen months of results on the 2025 axes. The movement is vertical.
Everything hill climbed. Almost nothing moved left.
October 2025 is the floor. An OpenAI executive announced that GPT-5 had solved ten open Erdős problems; Thomas Bloom, who maintains the problem list, called it “a dramatic misrepresentation” and explained that “open” on his site means he personally had not seen a paper solving it. The model had done a superb literature search. Demis Hassabis called the episode embarrassing. The posts came down. That is pure rediscovery, and it is worth remembering as the baseline against which everything since should be measured.
Eight months later the same class of system produced a counterexample to a 1946 Erdős conjecture, then a counterexample to a 1939 one, then a proof of a result that had defeated the field for two years. On outcome novelty these are not comparable to a literature search. On prior dependence, though, the Navier–Stokes result sits almost as far right as the Erdős embarrassment did. It inherited a direction, a strategy and a two-year research programme.
The Jacobian counterexample is the interesting outlier. Nobody handed the model a map to a specific region of a space with ten-to-the-117 members. That is the closest anything has come to the low-prior, high-novelty corner — and what came out was an object, not a theory. The corner reserved for a new framework, a new definition, a new way of seeing, remains empty. Edward Frenkel’s 2025 claim that these systems cannot produce conceptual structure has lost its strong form badly. Its weak form is still standing.
8. The four voices, thirteen months on #
Part I of this series set four positions against each other: Bubeck the optimist, Frenkel the sceptic, Ryu the careful middle, Nguyen the pragmatist. Each of those arguments has now been tested against events, and three of the four have moved in ways their authors probably did not expect.
Figure 7 · Where each of the four 2025 positions now locates the binding constraint.
The pattern across the row is that the binding constraint has moved off the model. None of the four now names capability as the limit. They name verification capacity, human attention, institutional conflict, and the slow work of turning a result into something teachable. Those are all throughput problems on the human side of the interface, which is precisely where my harness and token-economics work keeps landing.
9. The broker problem #
Here is the part of this story that my finance background will not let me read any other way.
A broker that sees client order flow and trades ahead of it is regulated. Not because anyone proved intent in a particular case — proving intent is close to impossible — but because the information asymmetry is structural. The remedy the market settled on has three parts: information barriers between the desks, mandatory timestamped records of who saw what and when, and a burden of proof that sits with the intermediary rather than the client. Good faith was tried first. It did not survive contact with incentives.
The frontier labs now occupy that seat. They supply the research tool and they compete on the research output, and in this case they mobilised a compute budget their own customer could not approach, on a problem that customer was days from finishing. OpenAI’s own statement concedes it cannot fully exclude an indirect channel. In markets, that concession alone is what triggers controls. Here, nothing triggers.
The symmetry of non-proof
Buckmaster cannot demonstrate that his drafts were used. OpenAI cannot demonstrate that they were not. Both statements are true simultaneously, and that is the exact condition recordkeeping regimes exist to eliminate. Financial regulators did not resolve this by asking firms to be trustworthy; they resolved it by making the audit trail mandatory and putting the cost of its absence on the firm. Mathematics has no such trail. The Leiden Declaration of June 2026 asked for disclosure and attribution. Disclosure is a promise. An audit trail is a control.
The cost figure points the same way. Millions of dollars of compute for one theorem is a terrible price per result and a cheap price per headline. Read it as a research budget and it looks irrational. Read it as marketing spend against a valuation and it looks disciplined. The Fields Medallists’ declaration is, at bottom, an objection to that reading of the objective function — the argument that mass-producing true statements at speed, with no write-up, no isolated method and no citation trail, can sterilise the ground it claims to be cultivating.
Whether you find that persuasive probably depends on whether you think the transmission chain between mathematicians is infrastructure or sentiment. I think it is infrastructure, and I think it is the kind that is cheap to damage and slow to rebuild. The counter-case deserves a hearing too, and the strongest version of it appeared in the comments on Tao’s own blog: hand those same notes to a dozen brilliant humans and they do not finish in four days either. The ability to connect, upgrade and complete at that speed is a real capability, whatever its provenance. Both things can be true.
10. What this is actually a result about #
Ten thousand concurrent agents. Reallocation as branches succeed or fail. Consolidated intermediate findings pushed back into the working groups. A separate formalisation stage on a different model. A comparator check to confirm the proof establishes the stated theorem.
That is an orchestration architecture. The model is one component of it.
This is the same finding my own experiments keep producing at a fraction of the scale, and it is the throughline of the harness work in my prior articles and “The Balance Sheet of Intelligence”: the structure around the model routinely delivers more lift than the next model upgrade. A single frontier model asked this question cold would have returned plausible nonsense. The result came from search breadth, a human-supplied direction, machine-checkable verification, and a feedback loop between them. Three of those four are engineering. One of them is a mathematician.
The token figures make the point in a different currency. The Riemann bound cost 31 million output tokens. The Fermat formalisation cost roughly six billion. OpenAI has not published a token count for Navier–Stokes, only Mark Chen’s remark that the compute bill ran to millions of dollars. Those three numbers span about two orders of magnitude for results of broadly comparable prominence, which tells you the price is set by how the work is organised rather than by how hard the mathematics is.
11. What I would watch #
Predictions in this area age badly, so here are markers instead — each of them resolvable, each one telling you something different if it lands.
12. Going deeper #
This piece is a map. If you want the territory, the sources below are ordered by how much background they assume, and every one of them is free.
13. Where this leaves the spectrum #
A year ago the open question was whether these systems could produce results that mathematicians would call “new”. Novel. That question is closed. They can, repeatedly, across combinatorics, algebraic geometry and fluid dynamics, and the people best qualified to judge have said so in public.
The question that replaced it is smaller-sounding and harder. Can they choose which question to ask? Every major result of the last thirteen months arrived with a human pointing at a target — an ansatz, a programme, a conjecture someone had spent years deciding was worth attacking. Tao’s warning about incentives lands exactly here: if a promising direction attracts ten thousand agents the moment it leaks, researchers will stop mentioning promising directions. The input that is currently scarce is the one the system is teaching people to stop producing.
That is the misalignment the twenty-five signatories are describing, and it has very little to do with how clever the models are.
One thing cuts against my own argument. If formalisation scales the way the Fermat result suggests — eleven days for a proof the field expected to take years, and a three-day formalisation of Vinogradov’s theorem done on three consumer subscriptions — then the verification column of my gap map shrinks fast, and the referee shortage that has bottlenecked mathematics since Kepler stops being the binding constraint. That would be an unambiguous good. It would also leave every other missing stage exactly where it is, because none of them is about checking whether something is true.
Appendix · How proofs become knowledge #
This piece has been about one result. The appendix is about the machine that used to turn results into knowledge, what that machine actually did, and which parts of it have stopped running. A general reader will get more out of the September story from these four diagrams than from any amount of detail about vortices.
A.1 The old machine #
A theorem became knowledge by passing through roughly eight stages, and only one of them was about establishing that the statement was true.
The other seven were about transmission. Someone decided the problem was worth attacking, which is a judgement built over a career. Someone had the idea. Someone wrote it out so that another expert could follow it. It circulated in preprints and seminars, and errors surfaced there — the gap in Wiles’s Fermat proof was found in the months after his 1993 announcement, during exactly that stage, and not in formal review. Referees gated it. Then the field spent years finding shorter routes, supervisors spent decades turning it into a course and then a textbook, and eventually the method escaped into other fields as a tool people picked up without knowing where it came from.
Figure 8 · The classical pipeline: eight stages, two feedback loops, and ten to forty years.
Notice who does the work. Every stage after the fourth is performed by people who did not write the paper, are not paid for it, and receive almost no credit. Nobody designed that arrangement and nobody owns it. It is also the only reason a result written by six people ends up understood by six thousand.
A.2 Five cases that already stress-tested it #
None of this is a defence of the old system’s speed. It was slow, and it had already been embarrassed repeatedly by precisely the problem now at issue: output that machines could produce or check faster than people could absorb.
The Kepler case is the one to hold on to. Twelve referees, four years, and the honest verdict was ninety-nine per cent. Formalisation is what finally closed it, sixteen years later. Lean is not a threat to that tradition — it is the answer the tradition was already reaching for. What is new in September 2026 is the ratio. Hales needed sixteen years to reach machine-checked certainty. OpenAI needed seventeen hours.
Fermat closes the same loop from the other end. The first row of that table is the proof Wiles published in 1995, which the community has been working to formalise since 2024. On 4 September 2026 a model finished it in eleven days. Every case in the table is a story about verification being the bottleneck, and they now all have the same answer.
A.3 The September machine #
Run the same eight stages against the calendar and the shape of the problem becomes obvious.
Figure 9 · Seven days for the stages a machine can run; nothing at all for the stages that need people.
The stages that ran are exactly the stages a machine can run without asking anyone’s permission: execute the argument, check it, publish it. The stages that have not run are the ones that require a person to volunteer. There is no submission, no referee, no seminar, no shorter proof and no course. There is also no mechanism that would produce any of them, because the incentive to do that work was always credit, and credit for digesting a machine’s output has not been invented yet.
A.4 Where the gaps actually are #
Laying the two pipelines against each other gives a more useful answer than the headlines did. The honest scorecard has three intact stages, two that changed for the better or worse, and six that have not happened.
Figure 10 · Stage by stage, how much of the old process survived the new one.
Two things in that map deserve more attention than they have had. The first is that machine checking genuinely came out ahead: a proof assistant gives exactness that twelve referees over four years could not. The second is that this strength has a hinge. A kernel confirms that a proof establishes a formal statement; it says nothing about whether that statement is the theorem anyone meant, or which axioms were used to get there. Both are judgements somebody has to make deliberately. For Fermat they were made: the proof uses only Lean’s three standard axioms, and a comparator confirmed the statement matches Mathlib’s own. For Navier–Stokes they have not been, by anyone outside the company that produced the proof, whose repository labels its own review status self-assessed. The difference between those two sentences is four days and a decision.
The other pattern is that the missing six are all record-keeping and attention, not mathematics. Nothing in that column requires a breakthrough. It requires somebody to be responsible for it.
A.5 What the mathematicians are asking for #
Read the Leiden Declaration of June 2026, the Fields Medallists’ declaration of September, and Tao’s posts alongside each other, and they converge on six specific asks. None of them is a demand that the machines stop.
Figure 11 · Six proposed gates, where each would sit, and who has asked for it.
Five of the six are administrative. Declaring your direction before you announce costs a paragraph. Completing the bibliography before publication rather than after costs an afternoon. Publishing prompts and failed runs costs a repository. One of them, the statement audit, has already been built and run in public. Only the sixth — funding and crediting the people who simplify and teach — costs real money, and it is the one with no obvious payer.
Why this is not gatekeeping
The objection that the declaration is protectionism?, because it was made immediately and in good faith. The answer is in Figure 10. Nothing the signatories ask for would have slowed the September run by an hour; every gate sits after the proof exists. What they are asking is that the four days of machine work be followed by the four years of human work that used to follow everything else, and that somebody be named as responsible for it. A field that publishes true statements nobody has digested is not a faster version of mathematics. It is a different activity that happens to use the same notation.
That is the shape of the problem, and it is not confined to mathematics. Any profession where years of training exist to produce judgement rather than output faces the same arithmetic: the output stage automates first, the judgement stage automates last or never, and the transmission stage in between quietly loses its staff. Law, clinical medicine, code review and audit are all on the same curve. Mathematics is simply the profession where the output is unambiguous enough that the gap is impossible to argue about.
References #
1. OpenAI, announcement of the Navier–Stokes result, 8 Sep 2026. https://openai.com/index/navier-stokes-solution/ 2. OpenAI, “Finite Time Blowup for Navier–Stokes” (166-page manuscript). https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf
**3.** OpenAI, companion Euler manuscript. [https://cdn.openai.com/pdf/315b36cd-ec98-4023-8342-93345194ece1/euler.pdf](https://cdn.openai.com/pdf/315b36cd-ec98-4023-8342-93345194ece1/euler.pdf)
**4.** OpenAI, Lean formalisation repository (review status: self-assessed). [https://github.com/openai/NavierStokesAndEuler](https://github.com/openai/NavierStokesAndEuler)
5. Alpöge & Buckmaster, Euler preprint. https://cims.nyu.edu/~tristanb/euler.pdf
6. Alpöge & Buckmaster, Boussinesq preprint (best starting point of the three). https://cims.nyu.edu/~tristanb/boussinesq.pdf
7. Alpöge, Buckmaster & Coiculescu, incompressible porous medium preprint. https://cims.nyu.edu/~tristanb/ipm.pdf
8. Buckmaster, personal statement on the sequence of events. https://cims.nyu.edu/~tristanb/statement.pdf
9. Córdoba & Martínez-Zoroa, the originating preprint (arXiv:2410.22920). https://arxiv.org/abs/2410.22920 10. Tao, “Finite time blowup with smooth forcing term…”, 7 Sep 2026. https://terrytao.wordpress.com/2026/09/07/finite-time-blowup-with-smooth-forcing-term-for-the-incompressible-porous-medium-boussinesq-and-incompressible-euler-equations/
11. Tao, “A Severe Misalignment of AI in Mathematics”, 11 Sep 2026. https://terrytao.wordpress.com/2026/09/11/a-severe-misalignment-of-ai-in-mathematics/
12. The mathematicians’ declaration and signatory list.
https://mathandai.org/
13. The Leiden Declaration on AI and Mathematics, June 2026.
https://leidendeclaration.ai/
14. Tao, crowdsourced list of general resources on AI and mathematics. https://terrytao.wordpress.com/2026/09/10/crowdsourcing-a-list-of-general-resources-on-ai-and-mathematics/
15. Burt Totaro (guest post), “On the Hodge conjecture”, 11 Sep 2026. https://terrytao.wordpress.com/2026/09/11/on-the-hodge-conjecture/
16. Tao, “Why global regularity for Navier-Stokes is hard” (2007) — still the best statement of the difficulty. https://terrytao.wordpress.com/2007/03/18/why-global-regularity-for-navier-stokes-is-hard/
17. Fefferman, official Clay problem statement. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
18. Clay Mathematics Institute, Millennium Prize rules. https://www.claymath.org/millennium-problems/rules/
19. Axios, “OpenAI’s historic math solution overshadowed by credit controversy”, 8 Sep 2026. https://www.axios.com/2026/09/08/openai-math-solution-navier-stokes-credit
20. WIRED on the compute cost and the academic reaction. https://www.wired.com/story/openai-navier-stokes-math-discovery-academics/
21. Scientific American, “OpenAI claims blockbuster math breakthrough amid swirl of controversy”. https://www.scientificamerican.com/article/openai-claims-blockbuster-math-breakthrough-amid-swirl-of-controversy/
22. The Economist, “Top mathematicians are outraged by OpenAI’s methods”, 11 Sep 2026. https://www.economist.com/science-and-technology/2026/09/11/top-mathematicians-are-outraged-by-openais-methods
23. Kingy AI, rolling evidence dossier on the claim and the dispute. https://kingy.ai/blog/navier-stokes-ai-proof-claims-dispute/ 24. Quanta, “Why the Legendary Erdős Problems Are Falling to AI”, 3 Aug 2026. https://www.quantamagazine.org/why-the-legendary-erdos-problems-are-falling-to-ai-20260803/
25. Kevin Buzzard (Xena Project), “Human mathematicians are being outcounterexampled”. https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/
26. Fortune on the Jacobian conjecture counterexample, 21 Jul 2026. https://fortune.com/2026/07/21/ai-solves-jacobian-conjecture-levant-alpoge-claude-fable-5/
27. The Decoder on the October 2025 Erdős episode. https://the-decoder.com/leading-openai-researcher-announced-a-gpt-5-math-breakthrough-that-never-happened/
28. Ganeshram, Duruisseaux & Anandkumar, unforced Euler project page (conditional result). https://tensorlab.cms.caltech.edu/users/anima/euler.html
29. Google DeepMind on machine-learning approaches to fluid singularities, Sep 2025. https://deepmind.google/blog/discovering-new-solutions-to-century-old-problems-in-fluid-dynamics/
30. Numberphile, “Navier-Stokes Equations” with Tom Crawford.
31. Terence Tao on the Navier–Stokes singularity problem (Lex Fridman Podcast clip).
32. James Maynard, short interview on the declaration.
33. Part I of this series — “When AI Proves Theorems and Tunes Detectors: Rediscovery, Synthesis, or (Novel) Discovery?” https://interestingengineering.substack.com/p/when-ai-proves-theorems-and-tunes
34. Part II of this series — “Prompting, Templates, and the Epistemology of AI Insight”. https://interestingengineering.substack.com/p/prompting-templates-and-the-epistemology
35. Hales et al., “A formal proof of the Kepler conjecture” — the completed Flyspeck project, August 2014. https://arxiv.org/abs/1501.02155
36. Hales, the original 1998 Kepler conjecture announcement. https://arxiv.org/abs/math/9811078
37. A critical retrospective on the Flyspeck formalisation. https://arxiv.org/abs/2402.08032
38. The Aperiodical’s account of Flyspeck’s completion. https://aperiodical.com/2014/09/the-flyspeck-project-is-complete-we-know-how-to-stack-balls/
39. Perelman, the first of the three Ricci flow preprints, November 2002. https://arxiv.org/abs/math/0211159
40. Anthropic, “Formalizing Fermat’s Last Theorem”, 4 Sep 2026. https://www.anthropic.com/research/formalizing-fermats-last-theorem
41. The Fermat proof itself, with a written walk-through. https://github.com/anthropics/fermats-last-theorem 42. Anthropic, “Claude’s progress on the Riemann hypothesis”, 10 Aug 2026. https://www.anthropic.com/research/riemann-zeta
43. Prove2Me, the coordination platform the Fermat campaign ran on (arXiv:2608.28433). https://doi.org/10.48550/arXiv.2608.28433 44. The Imperial College London community formalisation project for Fermat. https://github.com/ImperialCollegeLondon/FLT
45. Darmon, Diamond and Taylor — the exposition of Wiles that the formalisation follows. https://www.math.mcgill.ca/darmon/pub/Articles/Expository/05.DDT/paper.pdf
46. The Lean comparator used to check a formal statement against Mathlib’s. https://github.com/leanprover/comparator