Towards a Wiki For Formally Verified Mathematics

An anonymous reader writes "Cameron Freer, an instructor in pure mathematics at MIT, is working on an intriguing project called vdash.org (video from O'Reilly Ignite Boston 4): a math wiki which only allows true theorems to be added! Based on Isabelle, a free-software theorem prover, the wiki will state all of known mathematics in a machine-readable language and verify all theorems for correctness, thus providing a knowledge base for interactive proof assistants. In addition to its benefits for education and research, such a project could reveal undiscovered connections between fields of mathematics, thus advancing some fields with no further work being necessary."

Comments

Skynet

[Safiire Arrowny]

Skynet approves of this machine readable knowledge store.

Re:Uh ...

[Free the Cowards]

1. Russell did not, as far as I know, write any proofs in machine-readable language.
2. Goedel proved that such an endeavor cannot contain all true statements. But of course they never claimed that it would.

Maybe if you paid more attention you would be less amazed.

Re:Uh ...

[techno-vampire]

I'm no more of a mathematician than you are, but I've had the chance to discuss this with people who really do understand it. Your description is, I think, correct, but not your conclusion. What Goedel proved was not that such an endeavor was impossible, but that it could not be complete. This is because in any system sufficiently advanced to be interesting, there would always be some things that were true but which couldn't be proven to be true. (There would also, BTW, be things that were false but couldn't be shown to be false.)

Re:How much translation is needed?

[Chris Burke]

I don't know, all I know is that I have never been more tempted to vandalize a Wiki, in this case by replacing the middle steps of as many proofs as possible with "And then a miracle occurs..."

Re:Machine Readable ?

[TheEmptySet]

Hey. A lot of people devote a lot of their time in explaining their areas of mathematics to the general public (including myself). And as for your distaste for abstraction. That's what maths is! There is a reason the general public do not follow much in the way of mathematical developments and that is because research level mathematics is actually really hard and takes a lot of dedication to understand well. There is also no elitist clique. We love it when people show interest in our work and want to understand it.

Re:Uh ...

[zacronos]

Very close. To be 100% correct though, Goedel proved that any such endeavor would either be incomplete, or self-contradictory. In other words, for any sufficiently advanced system, there will be some things that are true but which can't be proven to be true within the system, or else there will be some things which can be proven to be true within the system but which can also be proven to be false within the system.

Re:Uh ...

[johanatan]

My apologies. [I had to brush up on the actual numbering system].

Correction: The Godel numbering system assigned a unique prime number to each symbol and axiom of his arithmetic. Then, the IDs of the combinations of symbols making up formulas were computed by raising each symbol or axiom ID to the power of its position in the sequence. And, finally, the ID of each proof or theorem by applying the same algorithm to the formula IDs making up each proof. More info here.

Re:Uh ...

[SoVeryTired]

"Goedel, Escher, Bach" is an absolutely astonishing book about this subject, and the foundations of logic in general. Applications to AI are also discussed. Admittedly, I had to stop reading it since it rather messed my head up (Got about 3/4 through and couldn't stop dreaming about maths). Highly recommended for any self-respecting geek.

http://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach

Re:Uh ...

[logicnazi]

I am a mathematician and in fact one who works in this area and what you say is pretty much correct.

More accurately what Godel showed is that no system complex enough to include arithmetic with a computable proof predicate is complete.

Let's take this apart and see what it means.

• Complex enough to include arithmetic: This means the system is complex enough to express standard questions in number theory e.g., for every even number > 2 there are two primes which sum to it and anything else that we can express by quantification over the relation of equality and the operations +, * and exponentiation. I could trivially make a complete consistent system which didn't allow you to express any interesting questions.

  More precisely the system must be sufficiently strong to prove a few basic facts about the integers and not prove false things about the integers.

• Computable proof predicate: In standard first order logic this simply reduces to the requirement that the axioms in the system must be in principal enumerable by a computer (which is equivalent to saying that there is a sentence in number theory with only a single existential quantifier that can answer whether something is an axiom or not). Without this restriction I could simply declare my system took as axioms all true arithmetical statements. Obviously though to qualify as the sort of mathematics we can verify and check it better satisfy this.
• consistent: The system doesn't prove both a statement and it's negation.
• complete: A system is complete if it admits a proof of S or ~S for every statement S in the language of the system. For instance a theory of arithmetic is complete if it proves or disproves every statement built up from basic arithmetic operations (+, *, exponentiation) via logical operations (and, or, not, existential and universal quantification).

-------------

People tend to make this whole thing way harder than it is. Here is a quick paragraph long sketch of Godel's first incompletness theorem.

Suppose there is a predicate P(s,p) which holds whenever p is an integer coding for a proof of the statement coded by the integer s (if you sit down for a few minutes you can figure out how to do the coding). Now suppose that P(s,p) can be expressed by a sentence in number theory involving only an existential quantifier, e.g, P(s,p) Ez(blah holds of s, p) where blah has no quantifiers.

Now it turns out that if you are a bit clever you can show that there is a sentence G so that

G holds iff (Ep)P('~G',p)

Where 'G' denotes the integer that codes for the sentence G. In other words G says "There is a proof that this statement is false".

Now suppose there was a proof of G. In this case it must follow that since the system correctly interprets arithmetic that there really is a proof of the negation of G. Hence both G and ~G have proofs so the system is incomplete. But if there was a proof of ~G then, as the system correctly interprets arithmetic, there is no proof of ~G. This is a contradiction. So neither G or ~G have a proof.

---------

The only hard part here is showing that G can talk about itself. The formal proof is pretty straightforward if we leave out the details. We define a formula F(n) (where n is a free variable) defined by:

F(n) n codes for a formula S(x) and (Ep)P('~S(n)',p)

Now consider the formula F('F'), i.e. apply F to the integer that codes for F. Expanding out the definition we see that

F('F') (Ep)P('~F('F')',p)

So we get our G simply by setting G = F('F'). To get an understanding about where you might get the idea to define F as this you need to understand that existential statements are really program and that this is really an application of the recursion theorem.

Re:Uh ...

[Ann Coulter]

Godel proved that Peano arithmetic is incomplete. There are some axiomatic systems that are both consistent and complete. Examples of such systems include plane Euclidean geometry and Presburger arithmetic.

Here are more examples:
http://en.wikipedia.org/wiki/Complete_theory