[FOM] Proving FLT in PA

[Timothy Y. Chow]

On Tue, 21 Feb 2006, joeshipman at aol.com wrote:
> Tim , one place you've seen it raised is on the FOM, by me, in 
> March/April 1999.

I did have a vague sense of deja vu as I wrote my last FOM message, but 
was too lazy to search the archives.

> What I would expect to see is a metatheorem of the form "pi^0_1 
> statements proved using etale cohomological facts X Y and Z applied to 
> sets of type A B and C are theorems of ZFC". That is, even if X Y and Z 
> need a strong assumption in order to be proven in their full generality, 
> the assumptions can be eliminated for applications of a certain type.

To put your expectation in context, let me say that one might also expect 
to see (1) a translation of SGA into English; (2) a more readable 
exposition of the material of SGA4, that is at the same level of 
generality and doesn't refer the reader to SGA4 for proofs.  Neither of 
these exists either.

We're talking hundreds if not thousands of pages of very technical 
material, so one has to be very strongly motivated to undertake the task 
of reworking it all.  Even many working algebraic geometers do not have 
the inclination to digest all of SGA.

The situation is similar in some ways to the classification of finite 
simple groups.  It's clear that the GLS project is an extremely valuable 
effort, but the way the mathematical reward system is set up, the GLS 
project is fueled by a significant dose of altruism.  Similar altruism 
will be needed before metatheorems of your type are proved.

Tim Chow