[FOM] Brief Reply to Comments on my Opinion 57

[Rob Arthan]

On Wednesday 12 Nov 2003 5:05 pm, Doron Zelberger wrote:
> 3) Reply to Ms. Kathy Garber
>
> >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?

Yes. E.g., see the work of Ursula Martin, Andrew Adams and others on using 
theorem provers to try to analyse the side conditions, e.g., on 
differentiability or definedness,  that computer algebra algorithms are 
inclined not to bother their little heads with.

>  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 don't know about philosophical implications or quite what you mean by "doing 
Heine-Borel". It's certainly a tremendous achievement that it is now possible 
to development large parts of analyis, algebra and topology in mechanized 
theorem proving systems. I would not have predicted things would have got so 
far when I first got involved in this area 15 years or so ago.

I don't think the treatment of this topic in Corfield's much-discussed book is 
balanced: he places far too much emphasis on _automatic_ theorem proving, 
where the machine is expected to do all the work, rather than _automated_ 
theorem proving, in which human and machine co-operate on the problem.

The Mizar project is the largest attempt at systematic development of a corpus 
of mathematics, although work has been done in these areas using HOL, 
Isabelle, PVS, NuPRL, ProofPower and other systems. Apart from Mizar, much of 
this work has been motivated by practical applications, e.g., verification of 
floating point algorithms.

> >
> >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?
>
> Interesting questions, Ms. Gerber. I have a great admiration to
> ATP, and read with great interest Donald MacKenzie's book
> `Automating Proofs', but I think that ATP have limited scope in
> creating new non-trivial math, since it is logic-based.

I'm inclined to agree with that as regards _creating_ maths. That said, I 
don't see any particular harm in rigour, personally.

> I prefer what I call ansatz-based math, which would emulate
> (much faster and better) the way math is actually created,
> as opposed to written up, in the stultifying Euclidean-Fregean
> style.

Unfortunately, though, the writin- up surely has to be done if results are to 
be believed. Even worse, the write-ups have to be reviewed and that may not 
be humanly possible. This has already happened in the case of Hales' proof of 
the Kepler sphere-packing conjecture. Not unsurprisingly, Hales is looking to 
ATP to solve the problem, see  http://www.math.pitt.edu/~thales/flyspeck/

> So ultimately CAS would be more promising, but they are
> still in a very primitive stage, and perhaps a synthesis of
> ATP and CAS would be fruitful.

I agree and so do many others, e.g., see http://www.calculemus.net/

Regards,

Rob.