From: Carlos Gonzalia (gonzalia@cs.chalmers.se)
Date: Thu Jun 20 2002 - 05:11:15 MDT
>From: "Lee Corbin" <lcorbin@tsoft.com>
>
>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?
Horribly late answer (sorry, both net access and work are driving
me nuts):
Not too good, and it probably doesn't terribly matter for now.
I think the FTA Project guys were mainly interested in showing
feasibility for a typical very complex proof, and also gaining
insights / finding some of the proper conceptual tools in
computer-assisted formal proof. I think they succeeded greatly
in both regards, both of which are still crucially important
points for us in the "logical frameworks" field.
The main thrust in the field right now seems to be (sensibly
so, IMHO) towards formalizations of mathematical theories that
involve interesting computational / constructive elements, and
for which the use of a computer proof assistant is a good idea
not only for the facilities provided by such a tool, but also
because the conceptual underpinnings of the logical frameworks
provide a very fruitful viewpoint for said theories. As a good
example of what are people doing, you can check the page of
our research group here, if I may be so immodest ;-)
http://www.cs.chalmers.se/Cs/Research/Logic/experiments.mhtml
/Carlos
This archive was generated by hypermail 2.1.5 : Sat Nov 02 2002 - 09:14:55 MST