AI proof to Navier-Stokes by the end of the year?

One of the things that took place in yesterday’s social media for me was the discussion around a 10,000$ bet between two DeepMind engineers, Marcus Hutter and David Budden (who left DeepMind to work on proving math stuff with LLMs). David bets that he can solve the famous Navier-Stokes existence and smoothness question, a Millennium Prize problem, by the end of the year.

The fact that this is a bet between two people that work in both AI and math, incited the spirits of the community. People are really excited to see if this is possible, given a recent streak of LLMs being used on Erdős problems. There was even a bet on the bet on Manifold’s prediction marketplace.

At the end of yesterday, David published a first version of the proof in Lean. Now, people can review this, find holes, and these could get patched before the upload of a PDF to arXiv.

There’s also a similar bet for another Millennium Prize problem, the Hodge conjecture. There is a published Lean proof too. But this bet is for the end of January.

There’s also a potential one for end of February on the BSD conjecture.

To be fair, I’m excited to see that these problems are getting tackled by a combination of GenAI and formal proofs in Lean. The burden of checking these is reduced, human reviewers don’t waste as much time as in the before times when mathematicians received proof manuscripts for these problems from various cranks (not calling any of the involved parties this). It might lead to more discussion, and more novelties.

For sure, AI lowers the barrier of entry, but due to the sycophancy problem it has, it can also generate a lot of noise. Whether you have a good or a crazy idea, the LLM will praise it the same. I’m looking forward to see how the remaining of the year develops, with regards to this debt.