Comment by ex-aws-dude
16 hours ago
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
16 hours ago
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.