8 ms·

How do you know the lean is correct? You don’t bet the two trillion dollar company on “the ai said so”

• adrianN 11d ago
  You carefully check that the problem is formalized correctly and then trust the Lean machinery to check the proof.
  • hodgehog11 11d ago
    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.
  • zarzavat 11d ago
    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.
  • wiz21c 11d ago
    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...
• krainboltgreene 11d ago
  I feel like that's exactly what's happened.
• eru 11d ago
  > 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.
• Almondsetat 11d ago
  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