On Thu, 25 Sep 2003, Michael Kleber wrote:
John, could you elaborate on why
... If it's combinatorial consideration of cases combined with elementary geometrical proofs of various numerical estimates, then I'll have strong doubts as to its correctness.
I mean, surely a proof along these lines exists -- the space of configurations (of 25 balls, possibly intersecting, all kissing a central one) is compact, so it can in principle be completely checked with a finite number of cases of the form "this configuration has at least epsilon overlap, so every configuration within distance epsilon of it is ruled out." k Yes, of course. The same argument applies to solving the game of Chess. If next week someone claims to have done that, I won't believe them for the same reason, namely that the problem is so big that their argument is more likely to be wrong than right.
This has very little to do with whether a computer is used, although that would of course improve the reliability. The trouble is that the problem is so big that a computer won't make much difference to its size, and I just don't believe that at the present time there's any real hope of finding a valid proof of this kind. On the other hand, I know full well that finding an invalid one is much easier, so, essentially for Bayesian reasons, that's what I'd confidently expect a claimed proof of this kind to be. The question is moot because fortunately Dan tells us that Musin's proof is of the second kind, which I expect to be short, simple, readily checkable, and therefore more probably correct. John conway