[FOM] Reply to Insall and Shipman on "100-year thesis" for computer proofs

[Koen Vervloesem]

In response to Matt Insall and Joe Shipman:

Regarding computer proofs, some mathematicians have made the conjecture
that eventually a proof will come up that is much shorter and much
easier to understand than the current proofs.

* Paul Halmos thinks that these computer-assisted proofs will become
"exercises in first-year graduate courses", when we will have found the
right level of concepts. Paul Halmos, ‘Has progress in mathematics
slowed down?’, The American Mathematical Monthly, Vol. 97, No. 7 (1990),
p. 577:

‘We may still be far from finding a “good” proof of the four-color
theorem. We need a simple insight into a new and complicated kind of
geometry or intricate algebra, and the distance from there to a purely
conceptual, existential proof of the four-color theorem is probably just
as great. […] I believe that the computer (and, for another example, the
10,000 pages of published proof solving the simple groups problem)
missed the right concept and the right approach. Their time will come. A
hundred years from now both theorems (maps and groups) will be exercises
in first-year graduate courses, provable in a couple of pages by means
of the appropriate concepts, which will be completely familiar by then.’

* Thomas Hales has the same hope regarding his computer-assisted proof
of the Kepler conjecture. He thinks the Kepler conjecture will become an
instance of a general family of optimization problems for which general
solution techniques will be found. Thomas C. Hales, ‘Some algorithms
arising in the proof of the Kepler conjecture’, Algorithms and
Combinatorics, Vol. 25 (2003), p. 489:

‘Ultimately, a properly automated proof of the Kepler conjecture might
be short and elegant. The hope is that the Kepler conjecture might
eventually become an instance of a general family of optimization
problems for which general optimization techniques exist. Just as today
linear programming problems of a moderate size can be solved without
fanfare, we might hope that problems of a moderate size in this family
might be routinely solved by general algorithms. The proof of the Kepler
conjecture would then consist of demonstrating that the Kepler
conjecture can be structured as a problem in this family, and then
invoking the general algorithm to solve the problem.‘

Kind regards,

Koen Vervloesem

On Sun, 2007-08-19 at 00:19 -0400, joeshipman at aol.com wrote:
> Yes, unless there is another counterexample (Dirichlet's theorem is
the 
> only unarguable counterexample so far, though I am currently 
> researching this to see how much of it can be made accessible).
> 
> Note that I did not propose that computer-aided proofs could be made 
> humanly readable within 100 years, just that anything the best human 
> mathematicians can do will be doable by undergraduates in 100 years. 
> The proof of the 4-color theorem is already accessible to 
> undergraduates now in the same sense it is accessible to any other 
> mathematician -- an undergraduate can easily understand the research 
> paper and verify the correctness of the program that checks the 
> unavoidable configurations for reducibility, and run the program. The 
> 100-year interval is the time scale for boiling down human knowledge 
> only.
> 
> Wiles's proof is being rapidly absorbed into an increasingly rich 
> theory, I fully expect it to be accessible to undergraduates by 2100.
> 
> Finite group theory is a good example of a field of mathematics with 
> lots of long messy unilluminating proofs, and I have no idea HOW the 
> proofs will eventually be simplified, but I discussed this with an 
> expert on the subject, John Conway, the other day, and he said he
feels 
> sure that much much better proofs exist and that we have just not, 
> collectively, been smart enough to find them so far.
> 
> (My 100-year rule is an empirical observation, but it may take longer 
> in the case of the CSFG, since it is a very unusual example of a 
> theorem proved by a huge collective effort without anyone really 
> understanding it all, and it is amazing that it really could be fully 
> accomplished by "crawling around", as Conway put it.)
> 
> -- JS
> 
> -----Original Message-----
> From: Insall, Matt <insall at umr.edu>
> 
> 
> In the year 2100, will proofs of the four-color theorem, the
> classification of finite simple groups, and Fermat's Last Theorem be
> accessible to undergraduates, by your thesis?