From: Technotranscendence (neptune@mars.superlink.net)
Date: Sat Jun 15 2002 - 13:12:58 MDT
On Saturday, June 15, 2002 2:10 PM Lee Corbin lcorbin@tsoft.com wrote:
>> 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!
I agree with Carlos here. Formalization has, in many areas, led to new
insights. Had it not been for people trying to formalize analysis in
the 19th century, a lot of modern maths, especially transfinite number
theory and set theory might not have come about -- or, more likely, been
delayed. Ditto for people looking to do the same with Euclid. If
someone didn't lie awake at night wondering about parallel lines and
proving Euclid right, how long would it have been before non-Euclidean
geometries came about and were embraced in physics?
Philip Kitcher covers some of this in his _The Nature of Mathematical
Knowledge_, a book I reviewed in the early 1990s in _The Thought_ and
then again with Stephen Boydstun in _Objectivity_. I highly recommend
his book.
Cheers!
Dan
http://uweb.superlink.net/neptune/MyWorksBySubject.html
Here's a photo of me from behind:
http://uweb.superlink.net/neptune/pic004.jpg
This archive was generated by hypermail 2.1.5 : Sat Nov 02 2002 - 09:14:48 MST
