3 ms·

Yes, but there's still the possibility that it's either exploiting a bug in Lean, or that the theorem statement is not set up correctly (i.e. it's actually prov

Yes, but there's still the possibility that it's either exploiting a bug in Lean, or that the theorem statement is not set up correctly (i.e. it's actually proved a different theorem). My understanding is that the theorem statement is quite simple, so i guess the latter is not very likely, but the former is very much a possibility in a proof this large, and it will take some human eyeballs to go over it before convincing mathematicians.

rawland 20d ago
I ran the proof 3 days ago. They do a Comparator Challenge to validate that they actually solved the correct theorem from the result, which they copied from Google/DeepMind: https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/ComparatorChallenges/NavierStokes.lean#L26 https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b... - this is valid for both Euler and NS. Also, they validated with an external kernel from the Lean Kernel Arena. That way bugs in the Lean kernels were found in the past already, iirc. Having said that, I strongly believe a positive result with the challenge above is the reason why they published it. I highly doubt anybody at OpenAI (or anywhere else) fully gets the proof after such a short time since publishing. This is also what Terry Tao criticized the most in my opinion. Independent of the remaining drama [0], from my point of view, the proof is correct and an achievement. [0]: https://news.ycombinator.com/item?id=49661928 https://news.ycombinator.com/item?id=49661928 - I am pretty much on the critical side, however, one can not ignore that it is an achievement. Esp. the unforced result.
HotHotLava 20d ago
Take a look at https://github.com/leanprover/comparator https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossible that they're hitting some bug, but way harder than one would intuitively think. For starters, they'd have to hit two bugs in two independently written Lean kernels.

rawland 20d ago

I ran the proof 3 days ago. They do a Comparator Challenge to validate that they actually solved the correct theorem from the result, which they copied from Google/DeepMind: https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b38b6e212696e8a30e3e91517af887bbd/ComparatorChallenges/NavierStokes.lean#L26 https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b... - this is valid for both Euler and NS. Also, they validated with an external kernel from the Lean Kernel Arena. That way bugs in the Lean kernels were found in the past already, iirc. Having said that, I strongly believe a positive result with the challenge above is the reason why they published it. I highly doubt anybody at OpenAI (or anywhere else) fully gets the proof after such a short time since publishing. This is also what Terry Tao criticized the most in my opinion. Independent of the remaining drama [0], from my point of view, the proof is correct and an achievement. [0]: https://news.ycombinator.com/item?id=49661928 https://news.ycombinator.com/item?id=49661928 - I am pretty much on the critical side, however, one can not ignore that it is an achievement. Esp. the unforced result.

HotHotLava 20d ago

Take a look at https://github.com/leanprover/comparator https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossible that they're hitting some bug, but way harder than one would intuitively think. For starters, they'd have to hit two bugs in two independently written Lean kernels.