6 ms·
LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.
by whateverboat 5d ago
LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.
- margorczynski 4d agoThis 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.