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

Second this. What I also wonder about is how closely the TeX write-up and the Lean formalization line-up.