logoalt Hacker News

whateverboattoday at 8:15 AM1 replyview on HN

LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.


Replies

margorczynskitoday at 11:22 AM

This is misleading. The proofs you speak of contained non-ZFC axioms and/or statements like "sorry". If the Lean proof conjecture is correct and it doesn't introduce any new axioms or use e.g. "sorry" then it provides a MUCH stronger guarantee of correctness than any peer-review done by humans.