the impression i get is that people don’t per se assert that exploitable bugs exist in Lean, but that the volume of (code) proofs published represent a new magnitude of challenge to the integrity of Lean.
the obverse would be to assert that Lean (or any other theorem prover) is infallible under all circumstances, present and future - an even weightier claim in my opinion.
the obverse would be to assert that Lean (or any other theorem prover) is infallible under all circumstances, present and future - an even weightier claim in my opinion.