4 ms·
So is there a chance that some of these AI-discovered proofs are actually Lean exploits?
by torginus 1mo ago
So is there a chance that some of these AI-discovered proofs are actually Lean exploits?
- ToValueFunfetti 1mo agoThis has happened: https://github.com/leanprover/lean4/issues/14576 https://github.com/leanprover/lean4/issues/14576
- qbit42 1mo 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.