Forgot your password?
typodupeerror
Math Social Networks The Internet Science

Towards a Wiki For Formally Verified Mathematics 299

Posted by kdawson
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."
This discussion has been archived. No new comments can be posted.

Towards a Wiki For Formally Verified Mathematics

Comments Filter:
  • Uh ... (Score:2, Insightful)

    by David Gerard (12369)

    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)

      by johannesg (664142) on Tuesday September 30, 2008 @06:24PM (#25210961)

      So Godel proved that Russell was wrong, then?

      • Re: (Score:3, Interesting)

        by mckinnsb (984522)
        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 pr
        • Re:Uh ... (Score:5, Informative)

          by techno-vampire (666512) on Tuesday September 30, 2008 @06:43PM (#25211155) Homepage
          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:Uh ... (Score:5, Informative)

            by zacronos (937891) on Tuesday September 30, 2008 @07:43PM (#25211841)
            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: (Score:3, Informative)

              by snarkh (118018)

              > 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

              • (although, admittedly most people choose to think of it as being true, whatever that means)

                Isn't that the purpose of the axiom of choice? :3

            • Re:Uh ... (Score:5, Informative)

              by melikamp (631205) on Tuesday September 30, 2008 @10:30PM (#25213379) Homepage Journal

              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)

              by Ann Coulter (614889) on Wednesday October 01, 2008 @12:05AM (#25214173) Journal

              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]

          • Re:Uh ... (Score:5, Informative)

            by SoVeryTired (967875) on Tuesday September 30, 2008 @08:09PM (#25212127)

            "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: (Score:3, Funny)

              by Fractal Dice (696349)
              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.
          • Re:Uh ... (Score:5, Informative)

            by logicnazi (169418) <logicnaziNO@SPAMgmail.com> on Tuesday September 30, 2008 @10:49PM (#25213575) Homepage

            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.

            • by logicnazi (169418)

              Crap the post pulled out my double headed arrows since it thought they were markup the last two formula should read

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

              and

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

            • Re: (Score:3, Insightful)

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

            • Thank you for that exposition, although I suspect you went into more detail than the average Slashdotter wanted. From what I gather, basic Arithmetic, with zero, positive integers but no fractions or negative numbers is complex enough if you include infinity.
    • Re:Uh ... (Score:5, Informative)

      by Free the Cowards (1280296) on Tuesday September 30, 2008 @06:24PM (#25210963)

      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.

      • yea, an axiomatic system doesn't have to be complete to be useful. most logical systems we use are incomplete, but their logical consistence still makes them incredibly useful in science, engineering, and even mathematical research. this Wiki won't make mathematical systems complete, but it can still help discover new theorems--and check to see that existing theorems are all logically consistent with each other.

        i mean, if you are working with boolean logic you accept that its fundamental axioms are true. t

      • Just for the record, if you're dealing with "machine readable language", what you want is the Turing Halting Problem, which is essentially the same mathematical derivation Godel used for theorems, but applied to algorithms.

        • You're only dealing with it if you're trying to decide if it halts (or if it's true, i.e. Godel's version).

          This wiki will not do that. It does not claim to do that.

          I don't understand why people cannot grasp this. All it does is automatically check a human-given proof that accompanies a human-given theorem. This is not revolutionary or even very hard. Why people feel the need to bandy about claims of mathematical impossibility is utterly beyond me. It has nothing to do with Godel's theorem.

          • There seems to be a large number of armchair philosophers in this thread and I salute you for trying to fix misconceptions!
    • Re: (Score:2, Informative)

      by RackinFrackin (152232)

      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.

      • Sweet, sweet example of this: the continuum hypothesis. http://en.wikipedia.org/wiki/Continuum_hypothesis [wikipedia.org]

        What this says is that there are "different" sizes of infinity. The "smallest" is that of the integers: -1, 0 , 1, 2 ...

        It is possible to show that one can never pair up every real number with a distinct integer. There are simply "too many" real numbers, and any attempt to pair the two sets up will result in real numbers being left over. In this sense, the set of real numbers is "bigger" than the integer

        • Of course, I'm wondering if they can import the contents of the Mizar electronic library for tracking the contents of the Journal of Formalized Mathematics (http://www.cs.ualberta.ca/~piotr/Mizar/mirror/http/library/), which would be pretty cool. The big questions are where the wiki and journal both stand on the Axiom of Choice. Some of the corollaries to the axiom of choice that show up in model theory (which has some interesting things to say about the dimension of the real line versus aleph numbers, be

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

      • 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

    • Firstly, those have nothing to do with this. Godel's theorem merely proves that there exists unprovable theorems that are true. In fact, Godel's theorem actually uses the fact that theorems can be verified in finite time - you just go line by line down the proof and check that it uses the axioms appropriately. This is a repository of theorems that are confirmable.
    • by logicnazi (169418)

      Godel's theorem tells us that ANY system that provides what we would intuitively call proofs is going to be either incomplete, inconsistent or too weak too be interesting. Godel's theorem applies just as much to the informal output of human mathematicians as it does to computer verified proofs.

      As a working mathematician my goal is always to produce arguments that convey enough information that the reader could turn them into a formal proof with enough time and effort. It would be a huge benefit if we coul

  • I'm not entirely familiar with machine verifiable proofs, but how much effort is needed to take a proof from www.planetmath.org and bring it up to standard for something like this? Obviously it'd depend on the thoroughness of the original proof, but I imagine a fair bit would be missing anyway. Also, would you be able to choose the axioms you're using?
    • by ceoyoyo (59147)

      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.

    • by Chris Burke (6130) on Tuesday September 30, 2008 @06:50PM (#25211223) Homepage

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

    • by Cyberax (705495) on Tuesday September 30, 2008 @06:56PM (#25211283)

      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]

      • by iabervon (1971)

        Have you ever tried to prove the properties of arithmetic? It's not hard, but it's tedious if you're starting from minimal definitions and have to prove that those definitions lead to the familiar properties. That is to say, bothering to prove those statements is not much less work in English than that, and people generally just don't have to do it, because it's already well established. But, of course, it's in the standard library for the prover, so you don't have to do it for the prover, either.

    • by exp(pi*sqrt(163)) (613870) on Tuesday September 30, 2008 @07:34PM (#25211723) Journal
      I can give a concrete answer. Browse metamath.org [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 [metamath.org]. 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.
      • Re: (Score:3, Interesting)

        by ceoyoyo (59147)

        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.

        • The link you provided looks like it's the LONGEST path they could find

          What you are implying makes no sense at all. There is no longest proof that 2+2=4 because given any proof, you can find a longer one. What they are doing is this: take metamath's proof that 2+2=4 (which is the result of lots of people working hard to find an efficient proof) and find the longest path you can take *drilling down* into that proof. In other words, the 150 is telling you that the best proof of 2+2=4 found so far is a tree 1

        • Re: (Score:3, Interesting)

          by tehcyder (746570)

          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.

  • Skynet (Score:5, Funny)

    by Safiire Arrowny (596720) on Tuesday September 30, 2008 @06:23PM (#25210951) Homepage
    Skynet approves of this machine readable knowledge store.
    • Re:Skynet (Score:5, Interesting)

      by Relic of the Future (118669) <dales@nOSPAM.digitalfreaks.org> on Tuesday September 30, 2008 @06:42PM (#25211137)
      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.

      • Re:Skynet (Score:5, Funny)

        by Chris Burke (6130) on Tuesday September 30, 2008 @07:40PM (#25211801) Homepage

        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.

  • Yay! Truth Mines! (Score:3, Informative)

    by seanellis (302682) on Tuesday September 30, 2008 @06:26PM (#25210987) Homepage Journal

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

  • Does this mean that Isabelle needs a formal proof to prove it works?

    • This is indeed what one would expect. For that reason I find matemath [metamath.org] far more interesting. Isabelle already has been use for some time. According to the wikipedia entry [wikipedia.org]: "It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness."
  • 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.

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

    • 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

      The math part you could do on a calculator...but what you really have seems to be a language problem. :)

  • without EMACS? Now that is progress.

  • One of the criticisms of mathematics is that mathematicians claim truth and rigour, yet in practise their proofs are often quite sloppy. In other words, most proofs are convincing rather than rigorous. Thus some have suggested that mathematics is made up of opinions rather than logically true assertions.

    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
    • One of the criticisms of mathematics is that mathematicians claim truth and rigour, yet in practise their proofs are often quite sloppy. In other words, most proofs are convincing rather than rigorous.

      Hear hear! How many proofs have you seen that are some variation of "Given the total body of known mathematical thought; the proof follows by inspection."? QED.

    • by eggstasy (458692)

      Normal math already uses unproven conjectures and hypotheses.
      There are things which seem fairly intuitive even to laymen but are very hard to prove.
      I am reminded of a theorem I learned about in college, that went unproven for ages: i think it was something like "given a closed loop, a point can only be either inside or outside it"
      http://en.wikipedia.org/wiki/Conjecture [wikipedia.org]
      http://en.wikipedia.org/wiki/Riemann_hypothesis [wikipedia.org]

    • by azgard (461476)

      Efforts like this one already exists.

      For example, there is Mizar system, which is a proof checker with about 46000 correct theorems in his database. So large parts of basic mathematics have already been formally verified.

      What is new in this project is the fact that it's a wiki, so anyone can add new assertions. That's improvement, and I believe that this openness will encourage all mathematicians to converge to some site like this in the future.

      This will ultimately benefit mathematics, because it will make

    • """
      yet in practise their proofs are often quite sloppy
      """

      And the people who say this are the ones that don't understand that each and every word has profound meaning. As in, in some books, it's not uncommon for someone who's learning, to spend an hour or more on one page unwinding it. Also, though some wording still may /appear/ sloppy, even after that, in the end, that "sloppy" wording is nothing more than a few lines of rigorous Math. You can't write *everything* out. Especially in a journal. It woul

  • I sounds like a great idea. So, umm, do it.

  • by davejenkins (99111) <slashdot@davejenkins. c o m> on Tuesday September 30, 2008 @07:29PM (#25211647) Homepage
    If you don't like this one, help yourself to the others (from wikindex.com, in order of activity):
    • http://www.exampleproblems.com/ [exampleproblems.com] ExampleProblems Wiki Graduate level mathematics example problems with solutions.
    • http://maple.wikia.com/ [wikia.com] Maple This page is all about the The Maple Wiki.
    • http://diffgeom.wiki-site.com/ [wiki-site.com] Diffgeom This wiki is about differential geometry and related facets of ...
    • http://www.mathcasts.org/ [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/ [wikia.com] Mathematics Wiki Mathematics is a Wikia for the collection of math-related news, ...
    • http://algorithm.wikia.com/ [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/ [wikia.com] GameTheory The Game Theory Wikia is a wiki about applied mathematics ...
    • http://matheaufgaben.wikia.com/ [wikia.com] Matheaufgaben Matheaufgaben Mathematics is a Wikia for the collection of math-related news, ...
  • Has anybody proven that?

    • There's the rub though, eh. The bugs that will *always* be in there... What will they do to the conclusions?

      Blindly trusting machines to do this (or close to it), when in the end it's Math that is depended on to see whether buildings will stand during an earthquake, etc, is irresponsible.

Do molecular biologists wear designer genes?

Working...