OpenAI claims to have solved a longstanding mathematical problem: the Navier-Stokes Problem. The Navier-Stokes equations describe the motion of fluids. The problem is this: given an initial state of the fluid (initial velocities of the fluid at every point and a field of forces acting on the fluid), is there always a “nice” (i.e. fluid-like)[1] solution to the equations?

This problem has eluded mathematicians for almost a century. It’s one of the Clay Institute’s Millennium Prize problems carrying a $1 million bounty. And yet OpenAI claims a swarm of 10 000 agents working for 88 hours at a cost of $15 million has found a counterexample — initial conditions with non-smooth solutions. The solution is being verified at time of writing, and there is some controversy as to whether OpenAI essentially stole the work of a pair of mathematicians who had recently made advances toward a solution and used it to train or prompt the internal model. But this post isn’t about that.

There has been a recent string of mathematical advances made simply by throwing enough compute at the problem. This seems to be yet another domain of human endeavour that faces losing its humanity as AI companies continue their crusade against culture, creativity, and community. It may be hard to appreciate if you didn’t get along with maths at school, but mathematics speaks to the soul in its own way. Understanding a mathematical theory is like appreciating great architecture. The individual struts, supports and rivets holding it together may not seem like much, but the structure is breathtaking when seen in its totality, an edifice of pure concepts. Then there’s the feeling of being lost, adrift and struggling, wondering what piece you are missing. On the other hand, eventually comes the ecstatic rush of finally penetrating a tough problem.[2] A machine feels none of these things. And it presents a real risk of denying it to humans.

The first instance of a machine proving something significant was the Four Colour Theorem in 1976, which says that four colours suffice to colour any map (as in a country map or similar) in such a way as no two adjacent regions share a colour. Kenneth Appel and Wolfgang Haken showed that the problem could be reduced to checking a finite number of map configurations, but since there were over 1800 such configurations, which had to be individually checked by brute-forcing possible colourings, there was no choice but to leave a computer to complete the proof. This took over 1000 hours. At the time, this was controversial — even if the computer’s proof was valid, it wasn’t “good” mathematics, because there was nothing illuminating or beautiful about it, and it had to be laboriously checked over by humans. While such concerns seem a little quaint now, they mirror the concerns felt by AI-critical mathematicians today.

Since then, computers have played a larger and larger role in theorem-proving. But of course, the vast capital expenditure in AI has increased the pace and scale of these contributions. Some contributions seem a natural fit for LLMs, in particular the translation of human proofs into formally verifiable computer proofs — this is essentially the same as turning a description of a program into an actual compilable program (for humans, this is generally extremely laborious and most proofs never receive this treatment). But in the last year or so AI companies have been claiming their products have solved significant problems, though it is generally unclear exactly what goes into these internal models and how much human assistance was required. Nonetheless, right now it seems inevitable that the pace of new AI-results will increase, and the amount of necessary human involvement will decrease.

Since we can’t put the genie back in the lamp, the best thing for mathematics will be if these tools remain mostly the domain of mathematicians using these tools to further their interests. As mentioned, the two real joys of mathematics are understanding theory and solving problems. If it turns out that AI is good at solving problems, it doesn’t mean it will be any good at building theories. In fact, it can’t be, because theories are novel ideas to further human understanding, and AI is not capable of serious novel ideas and it doesn’t know what future mathematical theories we could or should care about, or indeed, what is beautiful.

It may end up being that humans direct and build the theory, and AI crunches the proofs. It would still in this case be a bitter loss of the noble art of human proof, but it’s better than the alternative. The worst-case scenario is the sloppification of mathematics — AI companies and dilettantes with cores to spare churning out dross results for the prestige of having “proved” something, with no serious research program to guide them. A mathematical landscape as polluted with pointless results as the open source landscape is with pointless PRs, and the search rankings by pointless slop articles. And a planet all the more polluted by hyperscale data centres churning this pointless shit out.

I never did become a research mathematician. I lost motivation with my doctorate during the isolation of lockdown, and a stable everyday teaching job seemed more appealing than chasing postdoc positions and funding. I do regret not finishing the PhD. But seeing the probable direction of travel for research mathematics, I can’t say I regret not pursuing that career.

See also

  • Terence Tao has written about this a lot recently, including here, and also has several recent guest posts on his home page on this topic (archive link).

  1. Here meaning “smooth and with bounded kinetic energy”. ↩︎

  2. A famous photograph of Freud holding a cigar ↩︎