Want to read Slashdot from your mobile device? Point it at m.slashdot.org and keep reading!


Forgot your password?
Math Supercomputing Science

Achieving Mathematical Proofs Via Computers 209

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.

Achieving Mathematical Proofs Via Computers

Comments Filter:
  • by melikamp ( 631205 ) on Thursday November 06, 2008 @06:08PM (#25667407) Homepage Journal

    Godel of course proved that you can never have a complete list of all true statements in mathematics. So if they're just limiting it to "central" theorems, how do they decide what's central and what's not?

    Godel proved that you can never have a complete and recursive list of axioms for arithmetic. Regardless, "central" in TFA means well-known, which, IMHO, is fair enough. Letting a computer know proofs of all major results seems to be a necessary step on the way to building a silicon mathematician.

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

    by florescent_beige ( 608235 ) on Thursday November 06, 2008 @06:11PM (#25667459) Journal
  • Re:godelstheorem? (Score:2, Informative)

    by ComaVN ( 325750 ) on Thursday November 06, 2008 @06:11PM (#25667465)

    a formal system must be either incomplete or inconsistent -- and we do not really know which one applies to mathematics --

    Except that we do, and it's incomplete.

    Now, as to which applies to meatbags, my guess is they're both incomplete and inconsistent.

  • by fractic ( 1178341 ) on Thursday November 06, 2008 @06:15PM (#25667509)

    No, in general formalizing a proof does not require a lot of computer power. Usually it takes a lot of man power instead. Most current proof assitants are actually proof verifiers. The user has to break down the proof to elementary steps that the program can verify.

    Now sometimes a computer is used to verify a lot of cases by brute force computation. Often this is not done in an actual proof assistant but within a computer algebra package. But this is also met with a sceptical eye.

    The four colour theorem is perhaps one of the most famous formalized theorems. It was orginally proven by a large computation. But noone could really verify this. Recentely (2004) it was formalized completely in the proof assistant Coq (actually a custom extension). This formalized proof did require a lot of computer time allthough just on a normal computer, not a supercomputer.

  • by l2718 ( 514756 ) on Thursday November 06, 2008 @06:16PM (#25667527)
    In fact, Godel proved the exact opposite: that you can make a list of all true statements of mathematics. Godel's completeness theorem states that every statement that follows from the axioms is in fact deducible from the axioms in finitely many logical steps. It is thus possible to enumerate all true statements by enumerating all deductions. Godel also has proved an "incompleteness" theorem. That more famous (and less important) result is that there are statements that are true in specific models yet not provable from the axioms. It implies that there is no algorithm to decide whether a given statement is true -- but this has nothing to do with enumerating all true statements. (Yes, I am a mathematician)
  • Re:godelstheorem? (Score:5, Informative)

    by exp(pi*sqrt(163)) ( 613870 ) on Thursday November 06, 2008 @06:27PM (#25667685) Journal

    We already know that a statement like the continuum hypothesis can be proved neither true nor false from ZFC. We don't need Godel's theorem to prove "incompleteness or inconsistency" when we have lots of practical examples of its incompleteness. So your claim of "don't know" is false.

    First order logic is consistent and complete. In fact, Godel proved this. Additionally, consider the set S of all possible propositions of set theory. Somewhere in the power set of S must lie the set of all true propositions. Just take these as your axioms. Voila, a formal system that is both complete and consistent. Your characterization of Godel's theorem is incorrect.

  • by Manchot ( 847225 ) on Thursday November 06, 2008 @06:34PM (#25667783)
    There's a website called Metamath [metamath.org] which does a lot of what the article is talking about. It starts from the ZFC axioms and works its way up to thousands of elementary theorems, all proved completely formally. Pretty cool, if you're in to that sort of thing.
  • Um, no, no, NO! (Score:5, Informative)

    by Estanislao Martínez ( 203477 ) on Thursday November 06, 2008 @06:34PM (#25667787) Homepage

    Godel's completeness theorem states that every statement that follows from the axioms is in fact deducible from the axioms in finitely many logical steps.

    That Gödel's Completeness Theorem for first-order logic--predicates, individuals, quantifiers ("for all," "exists"), and truth connectives (not, or, and).

    Godel also has proved an "incompleteness" theorem. That more famous (and less important) result is that there are statements that are true in specific models yet not provable from the axioms.

    The incompleteness theorem is about arithmetic: natural numbers defined in terms of 0 and the successor relation, addition and multiplication. For any set of axioms you pick for arithmetic, there are true statements of arithmetic that cannot be proven from those axioms.

    It implies that there is no algorithm to decide whether a given statement is true -- but this has nothing to do with enumerating all true statements.

    I'm not completely sure of how relevant the incompleteness of arithmetic is for what you're saying, but I am sure of this: first-order logic is complete, but the validity of a statement in first-order logic is undecidable. Therefore, you don't need to bring in Gödel's incompleteness theorem for arithmetic to conclude that in many important cases.

  • by bcrowell ( 177657 ) on Thursday November 06, 2008 @07:17PM (#25668427) Homepage

    Which central theorems aren't already proven? Principia Mathematica did the basics and I always assumed more advanced theorems became proven as required. Maybe someone just wants to do Principia Mathematica volumes II through L but doesn't that already in effect exist?

    Well, one issue is that the Principia Mathematica undoubtedly has errors in it. No human being could ever write a book of that length without making a single mistake. So there could be some value in producing the same results on a computer, which doesn't make the same kind of mistakes a human does. Another issue is that the Principia Mathematica works within a certain axiomatic framework, and I believe that framework is different from the most popular axiomatic framework used today, which is Zermelo-Fraenkel set theory, with the axiom of choice (ZFC). (They were both produced around 1910, but the WP article says that PM used a complicated system of types, which is probably different from anything in ZFC.)

    More broadly, for people who are interested in the foundations of mathematics, there's no clear way to decide that one set of axioms is superior to another. Some people feel that ZFC is too strong, because it asserts the existence of things that can't be explicitly constructed. Those people may be interested in seeing how much of mathematics can be proved using purely constructive methods. With a weaker set of axioms, some results may be impossible to prove, while others may be possible to prove, but the proofs may be extremely long compared to the proofs in ZFC -- so long that using a computer may be a real help.

    Still other people are interested in seeing what can be done in an axiomatic system that's stronger than ZFC. For instance, such a system may have sizes of infinities that are larger than the sizes of the infinities in ZFC, and they may even have creatures like the set of all sets. One thing that tends to happen when you try to make stronger axiomatic systems is that it becomes much more difficult to avoid internal inconsistencies. I can imagine that a computer could be helpful in finding things like that. If you're fiddling around with the computer proof system and it comes up with a result that 1+1=3, then you've learned something interesting: your set of axioms is bogus.

    One thing you really have to be careful about if you're working in this kind of field is that you don't want to inadvertently assume some result that someone else has proved in some other axiomatic system, and that seems obvious to you, but that actually isn't provable (or hasn't yet been formally proved) in the system you're working in. That's the kind of thing where I'd imagine a computer system would be really helpful. It wouldn't allow you to make those assumptions. In general, if you look at almost all published mathematical work, it never states which axiomatic system it's assuming, and that's because in most fields of mathematics we expect that the results are unlikely to depend on which particular foundation you're working in. E.g., I doubt that Wiles' proof Fermat's last theorem even bothers to state that it starts from ZFC, and most mathematicians probably have a strong expectation that it doesn't matter whether you pick some other foundation, Wiles' proof will still be valid. Nevetheless, it's possible that that's not true. Abraham Robinson, for example, claimed that ZFC had been carefully engineered to make the real number system work correctly, and therefore claimed if you wanted to use a different system of numbers (such as the hyperreals, a system that includes Newton- and Leibniz-style infinities), you might be better off using diffrent axioms.

  • by sustik ( 90111 ) on Thursday November 06, 2008 @07:38PM (#25668773)

    > Godel of course proved that you can never have a complete list of all true statements in mathematics.

    Bzzzt. Wrong.

    What Godel proved was that all mathematical thruths cannot be described by a finite axiom system. The statement that there is a single empty set cannot be proved. Similarly continuum = aleph_1 cannot be proved; in both cases one may argue that these are so "obvious" that they need to be accepted as axioms.

    Note that continuum = aleph_1 was a strongly accepted conjecture as much as the Riemann hyp today.

    I studied set theory and models. It is fascinating that you can have a countable model of set theory! This model is basically built from a countable set with countable many subsets accepted as sets, etc. The rest of the subsets an "outsider" can see are not known inside the model. We denote this model (which is a counatble set for the ousider aka meta theory) by M. The natural numbers are in M, denote it by A. A is known in the model and A is an infinite (countable) set.

    The set containing the subsets of A, denoted by P(A) is different depending on whether you look inside or outside the model! Outside it is an uncountable set, of course. In the model world it is Pm(A) and it appears uncountable again, but for the outside observer it is actually the intersection of P(A) and M. Bear with me another minute!

    In the model world of M the Pm(A) appears not countable. What does that mean? It means that there is no 1-1 mapping between A and Pm(A). In the outside there is a mapping of course, since both sets are countably infinite. This mapping (a function) is actually a set (everything is a set: function, relation etc.) so a mapping denoted by F between A and Pm(A) exists outside. However F is not an an element in M so it does not exist inside the model.

    There is a way to extend the model M into something called M(F) by 'forcing' F to be in M. Basically we add F and everything else that need to be added to still have a valid theory inside M. It is not trivial to do this, it was discovered and proved by P. Cohen an analysis guy (not a set theorist). Set theorists of course run with this ever since. The careful picking of F allows different M(F)-s to be created and that leads to results showing that continuum = aleph_1 is not the only possibility. One can 'force' a bunch of other alephs under the continuum. (What aleph exactly can continuum be is also interesting to set theorists at least.)

    Now there is one model called L which consists of the 'constructible' sets and nothing else. In L continuum=aleph_1. There are in fact theorems based on the assumption that V = L, that is V the world consists of only constructible sets.

    You may wonder how this L can be defined. I cannot go into the details, but one eye-opening fact though is that you can define Lm inside the above M model!!! This Lm is a countable model of L and in some sense a minimal model of set theory if I recall correctly.

    So one may take the position that we want mathematical thruths in L the minimal system. (This resonates with Occam's razor.) Of course note that there is no axiomatic system describing L.

    I want to emphasize that if we fix a model then each statement has a truth value; but there exist truths which cannot be proved working inside the model only.

    For the usual applied math we could say we assume V=L. (Or any other well defined model for that matter.) Note againg that aleph_1 == continuum in L, because there are no other alephs that could fit "between". The mathematicians inside L see this as this: we cannot prove that aleph_1 == continuum in fact there could be something between, but it is not constructible from what we have.

    I hope this helped.

  • Re:godelstheorem? (Score:5, Informative)

    by kohaku ( 797652 ) on Thursday November 06, 2008 @07:47PM (#25668879)
    Why should AI be impossible? Surely it must be possible, with the human brain as evidence? One might argue that the brain is merely a biological computer not fully understood. Unless there is a "higher intelligence" giving humans beings thoughts, then AI must be possible. I suppose this is analogous to a Human "telling" a machine what to think, though, and gives rise to the "who created the creator" argument, but that's getting a little offtopic...
    This comment is somewhat similar to one below [slashdot.org] for which I apologise, but I wanted to expand on the point slightly :)
  • by melikamp ( 631205 ) on Thursday November 06, 2008 @07:56PM (#25668991) Homepage Journal

    How would you even define a notion of "follows from the axioms" that didn't presuppose proof in a finite number of steps?

    GP is talking about a concept known as logical implication. A set of axioms logically implies a statement if that statement is true in every model satisfying those axioms. A model is a particular interpretation of a set of axioms. Say, if your only axiom is (For all x, For all y (x+y = y+x)) then an abelian group of order two is a model, and so is Z, and so is any mathematical structure where operation + is, in fact, commutative.

    "Provable" (or "deducible"), on the other hand, means that there is a finite sequence of formulas which constitutes a formal deduction of a statement from the axioms.

    As logicians, we work in the meta-theory, which is widely accepted to be ZFC. A model is just a certain kind of set. Giving a rigorous definition here would be excessive, but we can at least mention that models are "big" objects which include the universe of discourse. So a model for natural numbers omega would, naturally, include the infinite set omega. "A logically implies B" is a statement about how A and B relate in various models. Compare that to "B is deducible from A", a statement about existence of a finite formal deduction, which, in meta-theory, is a different kind of set. A deduction is literally a record of finitely many formulas over a finite alphabet.

  • Re:godelstheorem? (Score:2, Informative)

    by ComaVN ( 325750 ) on Friday November 07, 2008 @03:41AM (#25672699)

    Sorry, I was wrong.

"Well, social relevance is a schtick, like mysteries, social relevance, science fiction..." -- Art Spiegelman