[FOM] The QED Manifesto today

[Ian Grant]

On Wed, 28 Jan 2009 13:53:42 -0500 (EST)
"Timothy Y. Chow" <tchow at alum.mit.edu> wrote:

> What I think you want are examples where the computer more-or-less
> finds new facts on its own   

Doron Zeilberger has been claiming something like this for years. He writes Maple programs which output 'papers'. See http://www.math.rutgers.edu/~zeilberg/tokhniot/oCLT1 for an example. This formulae was not conceived by him before it was proved. This is from http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/georgy.html

Of course Maple is not a proof assistant except insofar as it computes, but Zeilberger's idea, as I understand him,  is that 'symbol crunching' produces theorems in the symbolic domain (i.e. purely syntactically) which would not be accessible to 'naked brain humans' operating in either the domain of discourse: real analysis, say, or just pushing symbols themselves. The paper http://www.math.rutgers.edu/~zeilberg/mamarim/mamarimhtml/real.html is interesting and provocative.

Ian