[FOM] Re: Doron Zeilberger #57

[Kathy Gerber]

FOM Listers,

I would very much like to see discussion on Mr. Zeilberger's core ideas
beyond response to the introductory paragraphs of his article.

For example, are there any thoughts on the notion of number crunching as a
special case of symbol crunching? The implications?

Has anyone worked seriously with an automated theorem prover in
conjunction with a computer algebra system?  What *are* the philosophical
implications; i.e., if these systems can do Heine-Borel, what more can
they do and should we all keep doing Heine-Borel over and over? (much less
decorating web pages over and over..)

I have tinkered around with Isabelle recreationally, but don't really want
to invest the time required to gain proficiency if there are sound
mathematical grounds for using a different prover.

Specifically, for Mr. Zeilberger - have you investigated the tools of the
automated theorem proving (ATP) community yourself and found them lacking?


With all due respect,
Kathy Gerber