|
|
Re: Brainstorming about STEM (was About Functions)
Posted:
Dec 24, 2011 12:23 PM
|
|
Wayne said:
- ---------------------------------
I like geometry. Let's start with Hilbert's axioms for Euclidean
geometry and prove a couple theorems and a couple statements that
look like they are theorems but are demonstrably false.
- -----------------------------------
I have no idea why this is a response to what I wrote, unless you like Dan and Kirby think that finding proofs and generating proofs are the same problem. They are not.
Generating proofs *is* like the flip side of the coin to automated proof checking, however, if the topic is truly "formal" theories (please note that qualification). This whole silly sub-thread started when I simply was trying to point that out to Dan.
It is either slightly ironic or intentional that you bring up Hilbert's Geometry axioms. It was shown relatively recently (2001) by Meikle & Fleuriot, that Hilbert's system, when truly formalized in computer code, cannot handle some of the proofs by Hilbert himself that relied on geometric intuition rather than the formalism (i.e., these particular proofs of Hilbert's were decidedly "non-Hilbertian".)
For those interested, here is a link to a paper which can be read free online, and gives a glimpse as to some recent thinking on the
topic: http://rsta.royalsocietypublishing.org/content/363/1835/2377.full
Therein is mentioned the ironic observation on Hilbert's
geometry and also the famous "V-E+F = 2" of Euler that Kirby likes so much, and how such "proving" might itself be automated.
Merry Christmas,
Joe N
|
|
