[FOM] Proving FLT in PA
Timothy Y. Chow
tchow at alum.mit.edu
Wed Feb 22 20:02:31 EST 2006
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.
More information about the FOM