4 ms·

It's formalized in Lean, isn't it? Do you also rely on a community of C++ experts to tell you whether a program compiles or not?

tired-turtle 14d ago
"Beware of bugs in the above code; I have only proved it correct, not tried it." — Knuth, 1977
mpardalos 14d ago
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 13d 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 13d 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.
gerdesj 14d ago
"It's formalized in Lean, isn't it?" If that's the current burden of proof required in your world for maths then that's fine! 't'ain't in my world: I want to see peer reviewed and published. Surely that's not too much to ask. Its not perfect but generally works rather well for maths. I'm not a sodding programmer so please don't assume everyone here is one. I'm not a mathematician either but I do have standards: Your counter argument is a poorly constructed and inappropriately deployed example of "proof by whataboutism".
- HotHotLava 14d ago
  In what world is peer review a higher standard than formal verification in Lean? Not in the world mathematicians have been living in for the past decades at least. Nearly all big theorems that have been formalized so far had been published beforehand, and it was usually regarded as a step up in rigor. Wrong results get published in peer reviewed journals all the time.
  - aarstid 13d ago
    I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth. As a former academic who has been there, the process is extremely arbitrary and variable. Are people aware that the “peer” refers not to a community or a committee, but literally to one random guy or maybe a couple with zero accreditation? And that the journal editor can do whatever they want with this peer’s “review” including completely ignoring it?
    - rcbdev 13d ago
      I keep thinking the exact same thing every time I'm asked to peer review a paper.
    - gerdesj 13d ago
      "I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth." OK but this member of the general public has at least subscribed to New Scientist since 1987, nine O levels, two A levels, two AS levels and a HND in Civ Eng. All pretty mediocre but I have a fair idea on how sciencing is supposed to work and how it ... actually works. Obviously, I ended up in IT. I should also point out that maths "peer reviewed" is a bit special. For example Mr Wiles went through quite a maelstrom before his proof of some dodgy marginalia was accepted as "true".
jltsiren 14d ago
Verification with Lean is a piece of empirical evidence that the proof is correct. The paper passing peer review would be another. But even together, those two would be insufficient to establish the claim. While it's a convenient to assume that mathematics deals with logical statements, any attempt to evaluate those statements relies on physical processes with both known and unknown failure modes. There cannot be a test that establishes it unambiguously whether a claim is true or false. In all nontrivial situations, mathematical truth is based on expert consensus. When a new claim is made, people will try to raise and resolve objections, until a consensus emerges one way or another. As for C++, all compilers are different. For any given compiler, there are valid C++ programs the compiler fails to compile and invalid programs it compiles without any errors or warnings. And now that I think of it, a new version of a compiler crashing with valid code earlier versions used to handle is the only class of compiler bugs I see with any regularity.
shakna 14d ago
Formalized in Lean, just five months ago [0], resulted in discovery of bugs. Just because Lean can compile it, does not mean it is safely proven. It is the start of a process to check whether something actually holds, not the end. [0] https://news.ycombinator.com/item?id=47759709 https://news.ycombinator.com/item?id=47759709

tired-turtle 14d ago

"Beware of bugs in the above code; I have only proved it correct, not tried it." — Knuth, 1977

mpardalos 14d ago

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 13d 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 13d 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.

gerdesj 14d ago

"It's formalized in Lean, isn't it?" If that's the current burden of proof required in your world for maths then that's fine! 't'ain't in my world: I want to see peer reviewed and published. Surely that's not too much to ask. Its not perfect but generally works rather well for maths. I'm not a sodding programmer so please don't assume everyone here is one. I'm not a mathematician either but I do have standards: Your counter argument is a poorly constructed and inappropriately deployed example of "proof by whataboutism".

HotHotLava 14d ago
In what world is peer review a higher standard than formal verification in Lean? Not in the world mathematicians have been living in for the past decades at least. Nearly all big theorems that have been formalized so far had been published beforehand, and it was usually regarded as a step up in rigor. Wrong results get published in peer reviewed journals all the time.
- aarstid 13d ago
  I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth. As a former academic who has been there, the process is extremely arbitrary and variable. Are people aware that the “peer” refers not to a community or a committee, but literally to one random guy or maybe a couple with zero accreditation? And that the journal editor can do whatever they want with this peer’s “review” including completely ignoring it?
  - rcbdev 13d ago
    I keep thinking the exact same thing every time I'm asked to peer review a paper.
  - gerdesj 13d ago
    "I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth." OK but this member of the general public has at least subscribed to New Scientist since 1987, nine O levels, two A levels, two AS levels and a HND in Civ Eng. All pretty mediocre but I have a fair idea on how sciencing is supposed to work and how it ... actually works. Obviously, I ended up in IT. I should also point out that maths "peer reviewed" is a bit special. For example Mr Wiles went through quite a maelstrom before his proof of some dodgy marginalia was accepted as "true".

jltsiren 14d ago

Verification with Lean is a piece of empirical evidence that the proof is correct. The paper passing peer review would be another. But even together, those two would be insufficient to establish the claim. While it's a convenient to assume that mathematics deals with logical statements, any attempt to evaluate those statements relies on physical processes with both known and unknown failure modes. There cannot be a test that establishes it unambiguously whether a claim is true or false. In all nontrivial situations, mathematical truth is based on expert consensus. When a new claim is made, people will try to raise and resolve objections, until a consensus emerges one way or another. As for C++, all compilers are different. For any given compiler, there are valid C++ programs the compiler fails to compile and invalid programs it compiles without any errors or warnings. And now that I think of it, a new version of a compiler crashing with valid code earlier versions used to handle is the only class of compiler bugs I see with any regularity.

shakna 14d ago

Formalized in Lean, just five months ago [0], resulted in discovery of bugs. Just because Lean can compile it, does not mean it is safely proven. It is the start of a process to check whether something actually holds, not the end. [0] https://news.ycombinator.com/item?id=47759709 https://news.ycombinator.com/item?id=47759709