4 ms·
This has happened: https://github.com/leanprover/lean4/issues/14576 https://github.com/leanprover/lean4/issues/14576
by ToValueFunfetti 21d ago
This has happened: https://github.com/leanprover/lean4/issues/14576 https://github.com/leanprover/lean4/issues/14576
- qbit42 21d agoI have never seen an AI or a human produce a false proof without explicitly using weird meta programming tricks that are very suspicious. No "good faith" Lean proofs have every been shown faulty, to the best of my knowledge. While the risk is non-zero, many of the AI companies are also trying to find bugs in the Lean kernel, so it is becoming very well stress-tested.