Automated Proof Checking

[Don Blazys]

I recently learned that there now exists software such as:

Hol Light, Metamath, Isabelle, Coq, and Mizar

that can check mathematical proofs,

and pretty much eliminate the possibility of human error.

 

Do we have any Hypographers who are proficient in using

such automated proof checking software ?

(I still need "finality" on a result that has remained in "limbo"

for well over a decade, and this just might be the ticket out.)

 

Also, on a more philosophical note,

does this mean that in the not too distant future,

machines will be able to make discoveries

and create original mathematics?

 

Don.

[Haech]

grandpa godel should have something to say about this

[sanctus]

Doesn't sound revolutionnary to me. Maple &friends do it since a long time, maybe just not with a special UI for. I mean, the only thing for checking a mathematical proof is to check the maths, something you can code into Maple...

 

So I would not expect any revolution from this.

[Don Blazys]

Grandpa godel should have something to say about this.

 

He does. Google searching "automated proof verification"

I found something called "Metamath Proof Explorer",

that employs "Zermelo-Fraenkel set theory"

from which it is possible to derive the rest of mathematics.

[Haech]

My set theory knowledge doesn't really extend past abstract algebra; I thought Godel's incompleteness theorems might throw a wrench into the problem of machine based proofs, but maybe not. I've already passed on doing formal calculus and algebra to mathematica; if something could start proving things for me, then all the better :hihi: (I highly highly doubt that it would be possible to prove high level theory without a quantum machine)

 

I'm as curious as the op on this one.

[sanctus]

So can you explain me in what these programs differ from Maple, Mathematica etc.?

[Haech]

Proving something is an entirely different creature from symbolic manipulation. I'm sure you can program something that "proves" 1+1 = 2 given a set of axioms, but say if you're going to prove the central limit theorem, ito calculus, or euler's equation, the steps are a little difficult to describe symbolically, especially if we're going all the way down to some basic set theoretic system. I'm not a logician so proving from a "first order logic system" is a little beyond me, but I've always thought that brute forcing all the steps in that order would take an infinite amount of computation.

 

Here is an item. I think the common example for a non-turing computable proof is finding a limit. Maple and Mathematica can both find the limit of (x+1)/x, but how can they prove it?

[Don Blazys]

There seems to be some disagreement over whether or not

"proof checking software" is sufficiently sophisticated to be "adequate"

in checking most "relatively simple" proofs.

 

Wikipedia says that such software can indeed be quite usefull,

while this article:

 

(CiteSeerX — Conditional Computing (what proof checking needs from computer algebra))

 

seems to say differently.

 

Also, "Wolfram Alpha" appears to be a very sophisticated and usefull tool.

I wonder if it can be used to check proofs?

 

Don.