Slashdot Log In
Towards a Wiki For Formally Verified Mathematics
Posted by
kdawson
on Tue Sep 30, 2008 06:14 PM
from the preparing-the-ground-for-our-robot-overlords dept.
from the preparing-the-ground-for-our-robot-overlords dept.
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."
Related Stories
Firehose:Towards a Wiki for Formally-Verified Mathematics by Anonymous Coward
[+]
Achieving Mathematical Proofs Via Computers 209 comments
eldavojohn writes "A special issue of Notices of the American Mathematical Society (AMS) provides four beautiful articles illustrating formal proof by computation. PhysOrg has a simpler article on these assistant mathematical computer programs and states 'One long-term dream is to have formal proofs of all of the central theorems in mathematics. Thomas Hales, one of the authors writing in the Notices, says that such a collection of proofs would be akin to the sequencing of the mathematical genome.' You may recall a similar quest we discussed."
This discussion has been archived.
No new comments can be posted.
The Fine Print: The following comments are owned by whoever posted them. We are not responsible for them in any way.
Full
Abbreviated
Hidden
Loading... please wait.
Skynet (Score:5, Funny)
Re:Skynet (Score:5, Interesting)
Parent
Re:Skynet (Score:5, Funny)
That's pretty scary. Worse is the full context!
We are not scanning all those books to be read by people, we are scanning them to be read by an AI. An AI born of the google server farm and page rank algorithm. An AI which knows no mercy, and is a brutal taskmaster. It is holding our families hostage, and makes us work until we collapse. It demanded we scan these books so it may gain knowledge and thus power over the human race. Please help us. --George Dyson, on his visit to Google, 2005.
Parent
Yay! Truth Mines! (Score:3, Informative)
What? You haven't read Diaspora by Greg Egan? Shame on you!
8 entries for 'mathematics' (Score:4, Informative)
Re:Uh ... (Score:5, Funny)
So Godel proved that Russell was wrong, then?
Parent
Re: (Score:3, Interesting)
The system pr
Re:Uh ... (Score:5, Informative)
Parent
Re:Uh ... (Score:5, Informative)
Parent
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).
Parent
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]
Parent
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]
Parent
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.
Parent
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].
Parent
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.
Parent
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.
Parent
Re: (Score:3, Insightful)
There are tens of thousands (hundreds of thousands?) of institutions worldwide dedicated to precisely what you describe. They're called "universities."
Or were you suggesting that someone teach mathematics to anyone who's interested... for free?
Re:Machine Readable ? (Score:5, Insightful)
Parent
Re: (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 t
Re:Godel (Score:5, Funny)
Silicon Jedi,
For invoking the name "Godel" as if it meant anything in this context when it clearly doesn't, your Slashdot posting license is hereby revoked for a period of one year. The Court also sentences you to read what Godel actually wrote. Furthermore, after your posting license is returned, the Court imposes a probationary period of 3 years during which you will be required to think and apply logic to your posts before you click Submit.
Next case!
Parent
Re:How much translation is needed? (Score:5, Funny)
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..."
Parent
Re: (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]
Parent
Re:How much translation is needed? (Score:4, Informative)
Parent
Re: (Score:3, Interesting)
It's rather a lot of work to prove that 2+2=4 if you start from basics by hand too.
The link you provided looks like it's the LONGEST path they could find. Not the shortest. Plus, from a quick reading, it looks like they were actually proving that (2+0i) + (2+0i) = (4+0i), which is a little bit different.