Comment by ex-aws-dude
10 hours ago
To ask a dumb question is there any chance there can be a bug in these generated proofs that makes it think its true?
Or is it the case that as long as you verify the initial statements you are trying to prove the rest doesn't matter
Lean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).