From: Lee Corbin (lcorbin@tsoft.com)
Date: Sat Jun 15 2002 - 12:10:45 MDT
Carlos writes
> [Lee writes]
>> my statement was really a claim that there *aren't* any "rigorous
>> guidelines to suggest that an apparently completely rational argument
>> may have a hole in it". Now in mathematics (in theory) every
>> demonstration can be reduced to axiomatics, and can hence be checked
>> for utter rigor. However, perhaps it isn't well known that this is
>> almost never done in practice. For example, proving the Fundamental
>> Theorem of Algebra has never (to my knowledge) been reduced to a
>> symbolic formulation together with a set of appropriate axioms; it
>> would be a gigantic mess, and no one would really learn anything from it.
> The FTA was fully formalized by november 2000 or so by the
> Foundations group at U of Nijmegen, using the Coq computer proof
> assistant. (I know because I was in the TYPES meeting where the
> result was presented... ;-) ).
For those wondering what the Fundamental Theorem of Algebra is,
it's that every polynomial equation of degree n with complex
coefficients has n roots in the complex numbers, e.g., every
quadratic equation has 2 roots. The proof is usually a page
or two in length, as in "What is Mathematics?" by Courant and
Robbins, or "Theory of Equations" by Uspensky. It takes about
an hour to master the proof if you really try and use a lot of
caffeine. Gauss or Argand is credited with the first proof,
according to St. Google, 1799 or 1815 respectively.
> I humbly disagree about both the "mess" and the "not learning
> anything about it" parts. I understand the project has given
> tons of insights about computer formalization of mathematics
> constructive proof, and logical frameworks. Not to mention that
> the resulting library of algebra concepts formalized along the
> way is going to be useful for many people in the area.
Amazing. Thanks for a most interesting addendum!
> http://www.cs.kun.nl/~freek/fta/
> http://www.cs.kun.nl/~freek/pubs/kneser.ps.gz
I guess that I should have used for my example, "Reducing Andrew
Wile's proof of Fermat's Last Theorem has never been reduced to
a symbolic formulation together with a set of appropriate axioms,
and, while you might learn a lot about formalization, it would be
amazing if you learned any number theory."
What do you think the prospects are for reducing much harder
theorems? If the FTA took all this work, I wonder how bad
Lindemann's 1882 proof of pi's transcendence would be?
Lee
This archive was generated by hypermail 2.1.5 : Sat Nov 02 2002 - 09:14:48 MST