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