The Millennium Problems are a set of the most important open problems in mathematics. so far only 2 have been solved: the Poincare Conjecture by Grigori Perelman in 2010 and today OpenAI released this https://openai.com/index/navier-stokes-solution/

The only problem is, that their AI didn't even come up with the solution itself. Mathematicians working on the same problem recently made big strides in solving the Navier Stokes equations, and their chat logs were scraped and used in training data before they could release the proof themselves.

Here is the unpaywalled statements of the Mathematician: https://mastodon.social/@tristanbuckmaster/117233413705701198

Western AI companies have been tackling a bunch of open problems and techbro chuds cannot shut up about it, this is just Marketing and the fact they have to steal real people's work to do so just proves it. They really want that IPO moneyyy capitalist-laugh

you are viewing a single comment's thread
view the rest of the comments
[–] 14 points 2 days ago (1 child)

i think it's entirely possible they've done this as well; providing a lean formalization is at least something that can be readily checked. i think that's the other half of what's interesting about this actually. the magic here might be applying something that can spit out a great many outputs, most of which are nonsense (LLMs), to something that is basically verified to be correct if it works at all (the lean proof verifier).

  • source
  • parent
  • hideshow 1 child comment
  • [–] 14 points 2 days ago

    also notable here is that the solution they claim to have proven follows from the kind of progress that Terry Tao published a few years ago that suggested finite-time blowup for the navier-stokes equations.

  • source
  • parent