Comment by hodgehog11
9 hours ago
Why would they send it out for "expert review"? Every time, they have just made the AI generate a Lean proof. In fact, it seems like the most plausible direction to NS is computationally assisted detection of a blowup solution, which has fantastic automatic validation.
Anthropic sent out its Fermat's Last Theorem result to an expert on formalizing Fermat's Last Theorem in Lean, for what that's worth.
How do you know the lean is correct? You don’t bet the two trillion dollar company on “the ai said so”
The surface of bugs in Lean is infinitely smaller than the human error involeved in a committee of peer reviewers. It's way more probable to say "it's proven because Lean says so" than "it's proven because a couple of reviewers said so".
Also, if a bug is found, all previosuly proven theorems can be reproven to immediately and conclusively find out if things went wrong somewhere
You carefully check that the problem is formalized correctly and then trust the Lean machinery to check the proof.
As the recent "proof" of the Collatz conjecture shows, that's not enough in an adversarial context. Human mathematicians don't submit proofs that take advantage of soundness bugs in Lean. AIs do.
Each word of your answer is carefully chosen. I'll add one sentence though: you let time do its job.
Of course there may be errors in lean, of course AI can take advantage of it, of course "carefully" is full of errors. So the only thing left is waiting to see if the result holds. And yes, it may take 30 years...
Exactly, and the advantage is that checking that the problem is "formalized" here is essentially isolated to verifying that the final theorem statement matches the claim. If there are no 'sorry's and the program compiles, then it has been proven. That's the point of Lean.
> You don’t bet the two trillion dollar company on “the ai said so”
Making an ill-advised press release hardly dooms the company. Just like the hugging face incident hasn't doomed OpenAI.
I feel like that's exactly what's happened.