When OpenAI announced an AI-generated solution to Navier–Stokes, one of the seven Millennium Prize Problems, the comparison that followed was inevitable: another human intellectual stronghold falls, the way chess and Go did. This guest essay on Terence Tao’s blog — by the philosophers Silvia De Toffoli and Eamon Duede — argues that the comparison is wrong twice over, and that the interesting question is not whether AI beats mathematics but what mathematics is for.

Not all answers are solutions

  • The essay separates two senses of the word “proof.” A logical proof is one a machine can check, step by step, with no understanding required — and OpenAI published a Lean formalization of the Navier–Stokes argument that does exactly that. Lean is proof-checking software; a “formalization” is the whole argument rewritten so a program can verify each step.
  • An intelligible proof is the other kind: one a mathematician can read, grasp, connect to what they already know, and build on. For centuries the two ran together, because no human produced a 166-page logical proof without first understanding why the result was true.
  • AI breaks that link. The authors’ claim is that a formally certified result can float free of any argument a person can actually understand — an “answer” rather than a “solution,” on their terms. They compare it to Deep Thought’s answer of 42.
  • That is not an argument against formal proof. They note the converse failure is just as bad: an elegant, intelligible argument that does not actually establish the theorem, which they illustrate with the history of the Kepler conjecture.

Mathematics is not a game

  • Chess and Go have a win condition. Mathematics has no checkmate, no adversarial structure with final victory — so “AI beat us at it” describes a contest that does not exist.
  • Problem-solving is one aim among several. The essay quotes Tao’s own list of others: developing theories, unifying areas, training the next generation, sustaining a community, producing work valued for its beauty.
  • AI separates those aims from the solving. The authors’ worry is the incentive that follows: if success narrows to certified answers, mathematics will reshape itself around “precisely those features that are easiest to benchmark and automate away.”
  • They situate the argument in the moment: 25 Fields Medalists have signed a declaration warning of a “severe misalignment” between AI companies’ goals and the mathematical community’s, and they point at the credit economy in mathematics as something that also needs rethinking.

What the thread adds

The 141-comment thread on Hacker News splits roughly into people who read the essay as goalpost-moving and people who read the reaction to it as misdirected grief.

  • sigmoid10 — the main charge: “This kind of argument is always dangerous, because it essentially resorts to moving goalposts… If you only define yourself by things AI can’t do yet, you’re about to have a rude awakening.” kaffekaka rejects the reading — “The authors are absolutely not saying ‘we are totally safe’” — and stabbles names the pattern as God of the gaps.
  • yazaddaruvala — proposes “purpose death” for the feeling of having spent a career on excellence that a machine now supplies, and narrates the post as one phase of grief on Tao’s part. Two replies push back hard: emerongi (“You’re making up a narrative about another person. You have no clue what’s happening to him”) and GPerson, who notes Tao’s public position on AI in mathematics has been stable since 2023 and points out the post is by two other authors, “which highlights the problem with doing so.”
  • YeGoblynQueenne — a correction worth keeping: chess and Go are not “solved” in the technical sense the comparison borrows. Solved means a known outcome and perfect play from any position — tic-tac-toe, Connect Four, checkers. What exists for chess and Go are engines that beat humans, which is not the same claim.
  • matherial and qbit42 — a pair of practitioner counterweights to the optimists. One asks where the payoff is if everyone is shipping ten times faster, and observes “we’ve gotten less ambitious, not more,” because prototyping is now cheap and commitment is not. The other, writing from inside academia, describes a job drifting “from open-ended brainstorming to prompting/digesting LLM output,” with credit systems breaking and colleagues newly afraid to share ideas.
  • niemandhier and magimas — on the quality of the output itself: the OpenAI proof “allegedly reads like written by someone in acid,” and a reader reports that frontier models on open-ended problems produce “semi intelligible gibberish” in prose while the code is checked, so nothing punishes the gibberish.
  • dash2 — the dissenting position from outside the discipline: mathematics has a social purpose beyond employing mathematicians, in which case a machine that gets the results faster “is surely very good news.” curt15 answers that the concepts that come out of proving things matter as much as the results, and that the current fight is not about computational tools in principle but about companies “caricaturing it in the public eye as a game they can ‘solve’ or ‘beat’ for headlines and valuation.”
  • busyant — names the thing the essay’s reframing asks people to accept: if research prestige moves from solving hard problems to explaining machine-generated proofs, being told that this is the meaningful work “feels like you’re handing me a participation trophy and telling me I came in 1st place.”

The question the thread kept asking

The essay has nothing to say about who pays for mathematics once a machine can produce the answers, and two commenters raise it in different forms: reisse asks whether public funding should be adjusted for AI breakthroughs, and notes the sports analogy fails because “the general public never paid for the specific match results” — math was funded on the expectation of wider payoff, so should tenure lines shrink, grow, or be redirected toward explaining AI results? moralestapia asks the harder version in a reply: “Why would my tax dollars go to fund someone’s journey on what’s essentially a hobby at this point?” svara says the essay’s core premise — that mathematics is for human understanding — “is assuming its conclusion,” and that it will be “extremely difficult to defend, against the economic value of not caring.”

A note on reading comments as evidence: HN handles are pseudonymous and the site publishes no per-comment scores, so the ordering here is HN’s own ranking, not a vote. This is a slice of the thread, not a consensus.