7 ms·

Can you elaborate on this further? Would this mean that Bentley's proof was in fact incorrect (i.e. not a valid proof at all) or that it simply didn't consider

• pdpi 11y ago
  The exact size doesn't matter nearly as much as the fact that it has a bounded size. That changes the algebraic structure your proof operates on — and proofs on finite fields are often either general or at least give you results that explicitly depend on the size of the underlying set.
• pdpi 11y ago
  The exact size doesn't matter nearly as much as the fact that it has a bounded size. That changes the algebraic structure your proof operates on — and proofs on finite fields are often either general or at least give you results that explicitly depend on the size of the underlying set.
• chriswarbo 11y ago
  I suppose different people may answer your questions in different ways, depending on how they define words like "proof" and "correct". I would answer like this: the proof was correct, but it was solving the wrong problem (unbounded ints rather than bounded). Inside a formal system it's relatively easy to understand what's going on; the real difficulties are at the boundaries: how do we build a formal model of a real system, and how do we translate formal results back to the original system? It's a lot like programming: manipulating data is easy, the problems are getting the right data and interpreting what the output means. In this case, the model didn't capture overflow; so the proof is valid for that model, but it's not a useful model for Java's ints.