On Thu, Dec 15, 2011 at 7:17 AM, Joe Niederberger <firstname.lastname@example.org> wrote: >> It would be nice if everyone could master these >> "abstractions" and the basic methods of proof, but few >> are motivated to do so. I hope my little video and my >> software will help a bit in this regard. > > I'm not sure why students at large would be interested in formal predicate calculus based proofs, but for the smaller populations that are, it seems a shame to not include the fundamental fact that once a formal system is adopted, the very act of generating proofs can be automated - you can write a "function" that given a number, hands back a proof corresponding to that number. > (Of course, many mathematician's balk at the notion that what they do is "computational" yuck!...) >
The ability to generate proofs is quite different from the ability to work backward from a conjecture still in need of proof.
In the tiny worlds created by tautologists, "generating proofs" becomes a simple operation indeed. Child's play.
Don't confuse this with the idea the Euclid's corpus might've been "generated" by one of today's IBMs running software written by Harvard grad students. Not so.