logoalt Hacker News

lumosttoday at 2:56 AM4 repliesview on HN

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


Replies

Almondsetattoday at 9:14 AM

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

adrianNtoday at 3:36 AM

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

show 3 replies
erutoday at 6:19 AM

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

krainboltgreenetoday at 3:55 AM

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