Theorem-proving machines

The Economist has a nice article on the status of computer-aided proofs of mathematical theorems. The Kepler problem (sphere-packing in 3 dimensions) was solved a few years back using computer programs to check the 100K cases left after analytical work (shout out to Tom Hales :-) and the article mentions a new proof of the four-color theorem.

Mathematics will likely evolve to be more like physics, with "black box" computer components in complicated proofs playing the role of experimental data. Frankly, I don't see how this is very different from the previous situation. We have always had to accept the non-zero probability that a proof might have an error or loophole in it.

R. Solovay (who retired from Berkeley and is here in Eugene now) recently found a problem with Nash's almost 50 year old proof of the embedding theorem that the community had overlooked (see note below). I may have played a small role in this as I had been reading A Beautiful Mind around the time Solovay moved to Eugene, and asked him about Nash and the embedding theorem. This may have gotten him interested in the proof...

In the end, our grip on reality (even mathematical truth) is Bayesian at best :-)

---

(John Nash)

Recently I was notified by an e-mail from Prof. R. M. Solovay of a fault in the last part of the published paper "The Imbedding Problem for Riemannian Manifolds" which appeared in 1956 in the Annals of mathematics. At first I didn't believe that he had really found a flaw in the arguments, thinking that he had just failed to follow the line of argument. But when I was forced to re-examine it I saw that indeed his critique of the argument was quite accurate. There was simply a gap in the logic of the attempted device for assuring the avoidance of self-intersections in the embedding of a non-compact manifold of n intrinsic dimensions in an Euclidean space of (n+1)*(n/2)*(3*n+11) dimensions.

In principle it is not very difficult to arrange for that, in the context of the means being used (as of the time of that original paper). But a rigorous argument would need to be given and it would seem that such a repair would take a different line from the scheme that was described but which was not correct.

Of course subsequent work by others has achieved results that need much less in terms of the number of dimensions for embeddings, at least for a sufficiently smooth given original Riemannian manifold for which the embedding is sought.

Enclosed here (below) is a copy of Solovay's note that drew my attention to the fault in the originally presented argument.