Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

True! This is what has me more excited about LLMs producing Lean proofs than written maths proofs. The Lean proofs can be proved to be correct, whereas the maths proofs require experts to verify them and look for mistakes.

That said, I do think there are lots of problems where verification is easier than doing the task itself, especially in computer science. I think it is easier to list tasks that aren't easier to verify than to do from scratch actually. Security is one major one.



Even there it's risky. LLMs are good at subtly misstating the problem, so it's relatively easy to make them prove things which look like the thing you wanted but which are mostly unrelated.


Yes, Lean only lets you be confident in the contents of the proof, not how it was formed. But, I still think that's pretty cool and valuable.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: