3 ms·
Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs. https://github.com/leanprover/lean4/issues
by IsTom 20d ago
Soundness bugs in lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs.
https://github.com/leanprover/lean4/issues/14576 https://github.com/leanprover/lean4/issues/14576