3 ms·
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 s
by ex-aws-dude 26d 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
- JPC21 26d agoSecond this. What I also wonder about is how closely the TeX write-up and the Lean formalization line-up.