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

[Timothy Y. Chow]

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 
>by then.

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 
  complete proofs.

(2027 is the 100-year anniversary of the Artin reciprocity law.)  Any 
takers?

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."

Tim