Slashdot Mirror

← Back to Stories (view on slashdot.org)

Towards a Wiki For Formally Verified Mathematics

Posted by kdawson on 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."

34 of 299 comments (clear)

  1. Uh ... by David+Gerard · · 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.

    --
    http://rocknerd.co.uk
    1. Re:Uh ... by johannesg · · Score: 4, Funny

      So Godel proved that Russell was wrong, then?

    2. Re:Uh ... by Free+the+Cowards · · 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.

      --
      If you mod me Overrated, you are admitting that you have no penis.
    3. Re:Uh ... by RackinFrackin · · 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.

    4. Re:Uh ... by mckinnsb · · Score: 2, Interesting

      No. I'm only a math minor/computer science major, but from my limited understanding on the subject (as it was related to me by one of my smarter professors), Godel showed that Russell's system could not encompass all true statements. The problem (simplistically) lies in what is *demonstrably true* and what is *provably true*. In particular, Godel showed that Russell's system would have problems with things that are demonstrably true, or what you might call "self-evident truths" in philosophy.

      The system proposed however, might find things that are true that people haven't thought about proving yet. I'm sure a mathematician could come along and give a more complete answer.

    5. Re:Uh ... by techno-vampire · · Score: 5, Informative

      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.)

      --
      Good, inexpensive web hosting
    6. Re:Uh ... by zacronos · · Score: 5, Informative

      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.

    7. Re:Uh ... by johanatan · · Score: 5, Informative

      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.

    8. Re:Uh ... by SoVeryTired · · 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

      --
      Slashdot: news for Apple. Stuff that Apple.
    9. Re:Uh ... by Free+the+Cowards · · Score: 2, 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.

      --
      If you mod me Overrated, you are admitting that you have no penis.
    10. Re:Uh ... by Free+the+Cowards · · Score: 3, 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.

      --
      If you mod me Overrated, you are admitting that you have no penis.
    11. Re:Uh ... by snarkh · · 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).

    12. Re:Uh ... by melikamp · · Score: 4, 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).

    13. Re:Uh ... by logicnazi · · 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.

      • 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.

      --

      If you liked this thought maybe you would find my blog nice too:

    14. Re:Uh ... by Creepy+Crawler · · Score: 2, Insightful

      Hmm. A lot of footwork to simply explain that there is no grammar in mathematics.

      --
    15. Re:Uh ... by Fractal+Dice · · Score: 2, Funny

      You know, Although I've seen it on many shelves (including my own), I'm not sure I've ever met anyone who actually made it all the way through that book. Perhaps its impossible to prove or disprove if it's really a good book.

    16. Re:Uh ... by Ann+Coulter · · 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

  2. Skynet by Safiire+Arrowny · · Score: 5, Funny

    Skynet approves of this machine readable knowledge store.

    1. Re:Skynet by Relic+of+the+Future · · Score: 4, Interesting
      Ha ha, yes, very funny... but if you read the slides from the site (specifically, slide 18) he makes reference to that very fact.

      We are not scanning all those books to be read by people, we are scanning them to be read by an AI. --George Dyson, on his visit to Google, 2005.

      --
      Those who fail to understand communication protocols, are doomed to repeat them over port 80.
    2. Re:Skynet by Chris+Burke · · Score: 4, 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.

      --

      The enemies of Democracy are
  3. Yay! Truth Mines! by seanellis · · Score: 2, Informative

    What? You haven't read Diaspora by Greg Egan? Shame on you!

    --
    Sean Ellis
    Follow OfQuack's antics on Twitter.
  4. Re:Machine Readable ? by ceoyoyo · · Score: 2, 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?

  5. Re:Godel by Free+the+Cowards · · Score: 4, 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!

    --
    If you mod me Overrated, you are admitting that you have no penis.
  6. Re:How much translation is needed? by Chris+Burke · · 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..."

    --

    The enemies of Democracy are
  7. Re:How much translation is needed? by caramelcarrot · · Score: 2, Informative

    And that's the beauty of it - it'd be impossible to vandalise because everything is checked!

  8. Re:How much translation is needed? by Cyberax · · Score: 4, 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

  9. Re:Machine Readable ? by TheEmptySet · · Score: 5, Insightful

    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.

  10. Re:Machine Readable ? by David+Jao · · Score: 2, Informative

    If they'd just make it a bit more accessible for the general public, and provide more examples of what they are doing, instead of abstracting everything and assuming everyone knew as much as them (or rather what symbols they are using to represent what they know), then maybe mathematics would be further advanced.

    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.

  11. 8 entries for 'mathematics' by davejenkins · · Score: 3, Informative
    If you don't like this one, help yourself to the others (from wikindex.com, in order of activity):
    • http://www.exampleproblems.com/ ExampleProblems Wiki Graduate level mathematics example problems with solutions.
    • http://maple.wikia.com/ Maple This page is all about the The Maple Wiki.
    • http://diffgeom.wiki-site.com/ Diffgeom This wiki is about differential geometry and related facets of ...
    • http://www.mathcasts.org/ Mathcasts Mathcasts are screencasts (screen movies) which are created and shared to improve the learning and teaching of mathematics. Mathcasts were originally called math movies and then Whiteboard Movies but when the term screencasts became popular mathcasts seemed like a great name for them.
    • http://math.wikia.com/ Mathematics Wiki Mathematics is a Wikia for the collection of math-related news, ...
    • http://algorithm.wikia.com/ Algorithm In mathematics and computing, an algorithm is a procedure (a finite set of well-defined instructions) for accomplishing some task which, given an initial state, will terminate in a defined end-state. The computational complexity and efficient implementation... Algorithm The Algorithm Wikia is a wiki for gathering the latest
    • http://gametheory.wikia.com/ GameTheory The Game Theory Wikia is a wiki about applied mathematics ...
    • http://matheaufgaben.wikia.com/ Matheaufgaben Matheaufgaben Mathematics is a Wikia for the collection of math-related news, ...
    --

    davejenkins.com |

  12. Re:How much translation is needed? by exp(pi*sqrt(163)) · · Score: 3, Informative

    I can give a concrete answer. Browse metamath.org, a similar project in which machine verified proofs are collected. Look at the vast amount of work required to prove even the most trivial things. For example check out 2+2=4. Make sure you drill down into the proofs of the theorems used, not just the top level. Converting real world mathematics into machine readable form is a vast endeavor. It's also something that doesn't interest mathematicians, so the collection of machine verifiable proofs will lag *centuries* behind the state of the art.

    --
    Doesn't it make you feel good to know that our freedoms are protected by politicans, lawyers and journalists.
  13. Re:How much translation is needed? by ceoyoyo · · Score: 2, 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.

  14. Re:Machine Readable ? by comingstorm · · 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:

    • For about the past hundred years, abstracting everything is what has allowed modern mathematics to become further advanced
    • If you go back before math got so abstract, things don't get easier -- they just get more complicated and arbitrary.
    • Notation looks scary if you're not familiar with it, but it's harder to learn the math without it. We've tried writing it all down in prose, and that seriously doesn't work.
    • Mathematicians aren't born knowing all of math and its associated notation; every time we go into a new subfield we have to learn all of that, same as you.
    • As a math guy, I would love it if more people were interested in learning and doing serious math. Many mathematicians devote their lives to trying to do improve this situation. So, if you've got some magical formula that'll make John Conway eclipse rock stars and hotel heiresses in the tabloids, then by all means let us know about it!
    • I won't hold my breath, though.

    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...

  15. Re:Machine proofs are a farce by QuantumG · · Score: 2, Funny

    A smug bastard who would rather point and laugh at you than educate?

    --
    How we know is more important than what we know.
  16. Re:How much translation is needed? by tehcyder · · Score: 2, Interesting

    It's rather a lot of work to prove that 2+2=4 if you start from basics by hand too.

    My six year old daughter has proved to my satisfaction that 2+2=4, simply by counting on her fingers.

    --
    To have a right to do a thing is not at all the same as to be right in doing it