Slashdot Log In
Towards a Wiki For Formally Verified Mathematics
Posted by
kdawson
on Tue Sep 30, 2008 05: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
Submission: 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.
Uh ... (Score:2, Insightful)
1. Bertrand Russell's Principia Mathematica got there first.
2. Godel proved the endeavour was impossible.
I'm amazed a mathematician proposed this.
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: (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 (a
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: (Score:3, Funny)
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: (Score:3, Insightful)
Hmm. A lot of footwork to simply explain that there is no grammar in mathematics.
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: (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.
Parent
Re: (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: (Score:2)
All Goedel proved was that there exist true statements that it can't prove. There are still many theorems it can prove. And the theorems it can't prove are all stuff like, "This statement cannot be proven."
Show of hands: Who here cares about the software's inability to generate theorems like that? Anyone? Didn't think so.
Re: (Score:2)
And the theorems it can't prove are all stuff like, "This statement cannot be proven."
While that might be true in some sense, that's not the whole story. As an example of an useful such theorem, Matiyasevich (using various people's results) has shown that there's no way to prove if certain Diophantine equations have solutions or not.
Strictly speaking, all this means is that you can write a Diophantine equation that encodes some statement like the one you stated. But this doesn't detract from the original point: there still exists some Diopnhantine equation for which we can't prove the existe
Re: (Score:2)
Re: (Score:2)
Any given mathematical fact falls into one of three categories:
All Godel did was prove that category 3 exists. Previously it was thought that all facts fell into either "true" or "false", and the challenge was figuring out which was which.
You seem to be talking about known mathematics which have not been formalized but are considered to be true. This is, from what I can see, a major target of this wiki. Such things are a major source of uncertainty
How much translation is needed? (Score:2)
Re: (Score:2)
When I last used a proof checker (about seven years ago) there was a bit of work involved. You have to translate everything into the symbols and relations understood by the proof checker.
As I remember it wasn't the most technical process. A lot of it was dealing with syntax errors. Really, it's a lot like taking a pseudocode algorithm, or a program written in one language, and rewriting it in a programming language with very similar structure but different syntax.
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: (Score:2)
Maybe if I added the "Miracle Axiom"?
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.
Re: (Score:3, Interesting)
My six year old daughter has proved to my satisfaction that 2+2=4, simply by counting on her fingers.
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!
Who will prove the prover? (Score:2)
Does this mean that Isabelle needs a formal proof to prove it works?
depends on kind of math. (Score:2)
there are some areas like formal logic and staff which is heavily set-theoretical (like point-set topology) where automated provers are already available. you probably can add most of the algebra as well. OTOH, things like analysis (real, complex, functional) is much harder to formalize, many proofs end up with "now take epsilon to 0", or "take n to infinity", you have to deal with countable vs uncountable infinities. I'm not saying it's impossible to formalize, only that that's much harder.
Zombie David Hilbert... (Score:2)
... laughs at your difficulties.
(but is afraid of zombie Kurt Gödel.)
Use for the rest of us (Score:2)
That sounds great, but when will there be a computer which can solve my real-life math problems which mostly revolve around when will I pass Bob if Bob is driving at a speed in miles per hour from a place to a place at a time and I start driving toward the first place from the second place at a speed in kilometers per hour at a time? My current method of polling 4th graders isn't working very well.
Does this mean I can use Isabelle.. (Score:2)
without EMACS? Now that is progress.
Liberatory Mathematics (Score:2)
Some "scholars" from the humanities have used this to suggest we develop a postmodern, liberatory mathematics, freed from the tyranny of logical proof, and thus from the oppressive hegemony of the modern
vapourware (Score:2)
I sounds like a great idea. So, umm, do it.
8 entries for 'mathematics' (Score:4, Informative)
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: (Score:2)
"Just my take on it, I'm interested in maths, but resent the way mathematicians try to maintain their elitist clique."
LOL. That's the funniest thing I've read all day. Thanks for that.
Re: (Score:2)
obtuse/esoteric dialogue (Score:2)
My experience with math professors is that most of them are able to present clear explanations of the subjects they're teaching without referring extensively to topics that are more advanced than the topics at hand.
On wikipedia, however, "obtuse/esoteric dialogue" seems to be the norm, and I have very rarely been able to understand a math article about a topic that I didn't already understand. I hope that this trend will eventually correct itself by better editing.
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: (Score:3, Funny)
A smug bastard who would rather point and laugh at you than educate?