[FOM] Reply to Insall and Shipman on "100-year thesis" for computer proofs
Timothy Y. Chow
tchow at alum.mit.edu
Wed Aug 22 13:06:27 EDT 2007
Koen Vervloesem <kvervloesem at gmail.com> wrote:
>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
I would personally conjecture the opposite. I'm wondering if we can make
this discussion more "interesting" by means of a bet. I would be willing
to bet (say, a dinner) *against* the following statement:
In the academic year 2027-2028, there will be numerous (say, at least
twenty) universities/colleges offering an undergraduate course (*not* a
graduate course or a cross-listed undergraduate/graduate course) in
which all the main theorems of class field theory are given with
(2027 is the 100-year anniversary of the Artin reciprocity law.) Any
Class field theory is a nice example because there has been intense
scrutiny of it and there are several different approaches. But, as Lang
says, the important insights don't get "superseded." There's no single
proof that's clearly the simplest and the best. And it is by no means
clear that an optimally short and transparent proof exists. The notion of
Erdos's "Book" or that it's always possible to compress proofs of
important theorems down to a single, simple, conceptual, optimal proof
seems to me to be an instance of the strong law of small numbers, and not
true in general.
Note that even if one believes that one can always find the "right"
concepts to find the "right" conceptual proof, it doesn't follow that
things can be brought down to the level of first-year graduate exercises.
Developing the "right concepts" may in itself require a long chain of
preliminary "right concepts."
More information about the FOM