From: Carlos Gonzalia (gonzalia@cs.chalmers.se)
Date: Sat Jun 15 2002 - 09:53:54 MDT
>From: "Lee Corbin" <lcorbin@tsoft.com>
>[...]
>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... ;-) ).
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.
http://www.cs.kun.nl/~freek/fta/
http://www.cs.kun.nl/~freek/pubs/kneser.ps.gz
/Carlos
This archive was generated by hypermail 2.1.5 : Sat Nov 02 2002 - 09:14:48 MST