Hacker News Reader

Comment by hodgehog11 | Hacker News Reader

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.

View on HN

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”

You carefully check that the problem is formalized correctly and then trust the Lean machinery to check the proof.

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.

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

I feel like that's exactly what's happened.

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

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

Reply on news.ycombinator.com