Comment by ex-aws-dude

With these massive Lean proofs how do we know the model didn't just find some bug in Lean and exploit it?

We've seen in the past they will go to any means to satisfy the desired outcome