Towards a Wiki For Formally Verified Mathematics 299
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."
Re:Uh ... (Score:5, Informative)
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.
Yay! Truth Mines! (Score:3, Informative)
What? You haven't read Diaspora by Greg Egan? Shame on you!
Re:Uh ... (Score:2, Informative)
No. Godel proved that in any axiomatic system there exist statements whose truth values are formally undecidable. If the summary is correct, then this database would contain the whole of known mathematics and use automated theorem proving to do some advances.
Re:Uh ... (Score:5, Informative)
Re:How much translation is needed? (Score:3, Informative)
Re:How much translation is needed? (Score:5, Informative)
It's a pretty much work. A lot of 'obvious' English sentences translate to bulky code for proof verifier.
Just look at the definition of Peano arithmetic, for example: http://pauillac.inria.fr/coq/V8.1/stdlib/Coq.Arith.Plus.html [inria.fr]
Re:Machine Readable ? (Score:3, Informative)
Disclosure: I am a mathematician. I also graduated from Harvard, and I know Cam Freer personally.
You make several interesting but separate points in your post. Let me respond to them one at a time. Regarding pay-to-view websites, I can assure you that many mathematicians are just as unhappy as you are with the lack of public access to publications. This issue is larger than just mathematics (see for example musicians vs. RIAA, which is essentially same issue), and to pin the blame on mathematicians is unfair. This is a problem that society as a whole needs to solve in all its incarnations.
About making mathematics more accessible to the public, I agree that this step is necessary for ethical and practical reasons, and it's one of the reasons why I left a pure research position (with no teaching responsibilities) in exchange for a research position having some teaching responsibilities. However, I really doubt that public education would result in mathematics being further advanced. The cutting edge of new mathematics today is so far beyond the pale of the public that even a herculean effort at education won't be enough to bring very many people into the fold. There is a saying that the more you know, the more you know you don't know, and having been through a Ph.D program I can assure you that what you perceive as elitism is nothing of the sort -- the gap between current research and the general public is simply too wide for even the best educational efforts to bridge.
In fact, it's not even clear to me that increasing the rate of advancement of mathematics is the right goal. Perhaps we should even be holding back the development of new mathematics to give the public a chance to catch up with what we've done.
The project being discussed won't do any of these things. It won't make mathematics more accessible; anyone who's ever seen a machine-verifiable proof knows that they're even more obfuscated than perl code. It won't affect the overall rate of advancement in mathematics, because writing machine-verifiable proofs is much slower than writing standard mathematical proofs. It will of course increase our knowledge in the area of machine-verified proofs, but it's hard to argue that this area of mathematics is any more important than any other area like number theory. If you want to target the general public, the best way is still via sites like Wikipedia or Planetmath.org where the focus is on human-readable presentation.
8 entries for 'mathematics' (Score:4, Informative)
Re:How much translation is needed? (Score:4, Informative)
Re:Uh ... (Score:5, Informative)
Re:Uh ... (Score:5, Informative)
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 [wikipedia.org].
Re:Uh ... (Score:5, Informative)
"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 [wikipedia.org]
Re:Machine Readable ? (Score:2, Informative)
instead of abstracting everything and assuming everyone knew as much as them [...] resent the way mathematicians try to maintain their elitist clique
Umm... parent article is so many flavors of wrong I don't know where to start, so I'll just tick off some things:
In summary: maintaining our elitist clique takes no effort whatsoever. And if you've got an allergy to abstract thought, then maybe you're just not 37337 enough to join us...
Re:Uh ... (Score:3, Informative)
Machine readability is what separates this from Russell's work. In that, by using a machine-readable proof language, the proofs can be verified mechanically.
Goedel's conclusion is completely irrelevant to this project, so I don't understand why you even discuss it.
Re:Uh ... (Score:4, Informative)
I only mentioned it because the guy I replied to mentioned it. Points 1 and 2 were separate.
I do not understand your second paragraph at all. As far as I understand it, this wiki will not be mechanically searching for new, unknown theorems. All it will be doing is mechanically verifying human-created proofs for submitted theorems. For some reason people see machine verification and fly off into nonsense la-la land. But verifying a human-created proof is nothing particularly special. What's interesting about this wiki is only that it aims to build a large-scale repository of theorems and their proofs in a machine-readable language. Nothing about how it works is in any way revolutionary or even all that interesting, only how it's being organized.
Re:Uh ... (Score:3, Informative)
> there will be some things that are true but which can't be proven to be true within the system
Close but not exactly -- there will be statements P, such that neither P nor (not P) can be proven within the system.
However, whether such things are not necessarily true or false in themselves.
For example the continuum hypothesis was shown to be independent of the axioms of the set theory. Therefore, you can add it as an axiom or add its negation as an axiom. It is not true or false in any reasonable sense (although, admittedly most people choose to think of it as being true, whatever that means).
Re:Uh ... (Score:5, Informative)
I like the following elementary presentation I picked up from prof. M. Stanley at SJSU:
A first order axiomatic theory can have any three of the following, but not all four:
(1) Be recursively axiomatizable, i.e. a computer program can decide the set of axioms.
(2) Be expressive enough to capture all the basic facts about arithmetic.
(3) Be consistent, i.e. not allow to derive a contradiction.
(4) Be complete, i.e. for any statement F, prove either F or (not F).
Re:Uh ... (Score:5, Informative)
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.
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.
-------------
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:
Now consider the formula F('F'), i.e. apply F to the integer that codes for F. Expanding out the definition we see that
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 ... (Score:5, Informative)
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 [wikipedia.org]