Achieving Mathematical Proofs Via Computers

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

Comments

what is a central theorem?

[Hatta]

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?

Re:what is a central theorem?

[jfengel]

TFA also says:

When it comes to central, well known results, the proofs are especially well checked and errors are eventually found. Nevertheless the history of mathematics has many stories about false results that went undetected for a long time.

In other words... maybe, just maybe, there's a hole in one of the theorems we use all the time, and an error would have severe ramifications. Or at the very least, there might be an opportunity lurking in an assumption we didn't realize we were making, like the way non-Euclidean geometry was just sitting there waiting to be discovered.

They're not really "limiting" it to central theorems, so they don't need a definition. But the more important (read, broadly-used) a theorem is, the more interesting it will be to have the proofs double-checked by a computer.

That computer proof may itself be wrong if the programmers are wrong, but as with the proofs we already have, it's just one more set of "eyes" looking for problems.

Re:what is a central theorem?

[Bromskloss]

on the way to building a silicon mathematician.

I think we have one at our department. He's, like, very stiff.

Re:what is a central theorem?

[sustik]

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

[QuantumG]

I honestly think they need to stop teaching the halting problem to freshmen CS majors. They're just too inexperienced to understand that theory and practice are two different things.. so this whole "limits of computation" thing stifles their enthusiasm.

Re:Tagged Supercomputing

[fractic]

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.

The exact opposite is true

[l2718]

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:The exact opposite is true

[melikamp]

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?

[AWhistler]

Not only that, but people should stop using this as a crutch in general. The journey is worth the effort, even knowing that you can never reach the end. This is why I agreed with Godel, Escher, Bach by Hofstadter and disagreed with The Emporer's New Mind by Penrose.

One of Penrose's conclusions was that any attempt at artificial intelligence is necessarily incomplete, so it won't be possible, while Hofstadter said that it is possible to successively approximate something intelligent, and we can learn a LOT about ourselves in the attempts, and that in itself is worth it.

At least that is one of the many things I got from the two books.

Re:godelstheorem?

[exp(pi*sqrt(163))]

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.

Metamath Proof Explorer

[Manchot]

There's a website called Metamath 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!

[Estanislao Mart�nez]

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.

Proof is discrete

[Estanislao Mart�nez]

Benchmarks have shown that Via processors have much lower floating-point performance compared to their competitors (i.e. Intel and AMD) so why exactly are they using Via chips to achieve mathematical proofs?

A formal proof is not a numerical calculation. A formal proof is, basically, a set of premises, a conclusion, and a set of steps that justifies the conclusion, given those premises and a set of rules that define your proof system. The premises and conclusions are logical formulas, which are basically symbolic trees, and the proof steps relating the premises to the conclusion are all discrete too. So there is no essential numerical calculation going on at any point here.

Re:godelstheorem?

[BitterOak]

One of Penrose's conclusions was that any attempt at artificial intelligence is necessarily incomplete, so it won't be possible, while Hofstadter said that it is possible to successively approximate something intelligent, and we can learn a LOT about ourselves in the attempts, and that in itself is worth it.

Not only that, but Penrose doesn't offer any actual proof that AI is impossible, merely speculative reasoning. Therefore it seems doubly important that we continue our attempts to advance AI. Firstly, that the journey itself is worth the effort, and secondly we really need to find out for ourselves if it is possible.

Important for the long term evolution of CAS

[starseeker]

CAS, or Computer Algebra Systems, represent one of the most useful tools for handling practical application of complex mathematics. The package Feyncalc, built on Mathematica and used for High Energy Physics, is one such example. The problem with using these systems is that they can't be trusted by the people using them. There is always that risk of "did the programmer do something that buggered this case" or "did they get that formula wrong when they translated it to code?" The traditional answer is a combination of by-hand verification and learning to "trust" certain abilities of some systems over time - lots and lots of use creates a certain confidence that the bugs have been shaken out of well-used functionality. But that lingering doubt remains - "is it REALLY right?"

There are philosophical questions at the root of this issue. On the most abstract level is the question of whether knowing something is true is important compared to knowing WHY it is true - purists might argue if we don't know the latter the problem isn't answered. I'll state up front that for the problem I'm interested in solving - KNOWING my answer to a problem is correct - I'm willing to trust a machine that is proven by humans to be able to verify proofs as correct to verify MY solution to a particular problem. Or, put another way, that once the correctness of the checker is proven all statements of correctness from that checker are also proven. This is not a universal assumption, but if one is willing to make it things get interesting.

Most proofs mathematicians attempt are not the types of problems posed by high energy physics - proving the solution to a specific integral is the correct solution would be of minimal value as a mathematical revelation. For the practical focus of scientific use of CAS however, the question of whether the system just gave the correct solution to that integral is all important. Moreover, the mathematical axioms behind the statement of correctness are not of immediate concern - they interest mathematicians, but the physicists want to USE that result. There's a contradiction here, because to be trustworthy in a mathematical sense the foundational system within which that integral was evaluated and what assumptions were made in the process MUST be considered. What to do?

Trustworthy computer verification of proofs offers an answer to this dilemma. A CAS designed to incorporate proof logic awareness into its core system and algorithms could be asked to produce a "proof" of its answer based on the steps it used to create that answer. This proof can then be subjected, just like any human written proof, to the rigors of verification. A human COULD (in theory) do the checking if they wanted to. In practice, an incorporated proof verifier could examine the CAS's proof for flaws. If none were found, for the specific problem in question, the user could then know that the answer they have IS correct, regardless of any potential flaws in the CAS (which will hopefully be reduced dramatically by the design rigors needed to implement routines that can support supplying the proof logic in the first place). The trust tree has been reduced to the proof verification routine and the software and hardware needed to run it, which is a MUCH smaller trust tree than the whole of the CAS.

The practical realization of such a system is probably decades in the future. It could be done only as an open source system, where the entire mathematical and scientific community contributed to an ever expanding body of trusted knowledge which could be built upon. Many extremely difficult problems would need to be solved - an immediate problem is how to organize mathematics into a coherent framework in a scalable way via computer. Category theory is probably the answer, but what does that mean in terms of system implementation? What about the programming language that must be put behind the mathematical definitions, even if the conceptual framework of Category Theory in Computer is addressed?

Re:godelstheorem?

[kohaku]

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 for which I apologise, but I wanted to expand on the point slightly :)

Re:godelstheorem?

[Draek]

One of Penrose's conclusions was that any attempt at artificial intelligence is necessarily incomplete, so it won't be possible

But wouldn't Godel's theorem imply that it'd be impossible to build a flawless, all-encompasing intelligence, not necessarily an imperfect one? fsck, even I as a human (allegedly the "superior" intelligence) sometimes feel that my decisions are based solely on the output of a Random() call in my brain rather than logical thought, no reason why a machine has to be different.

AI isn't about trying to build God, it's just about something that can learn new stuff, or at least that's my take of it.

Re:godelstheorem?

[jonaskoelker]

But wouldn't Godel's theorem imply that it'd be impossible to build a flawless, all-encompasing intelligence, not necessarily an imperfect one?

Gödel's theorem's concludes, simplified a bit, that it's impossible to know the truth, the whole truth and nothing but the truth about sufficiently complex math. In this context, sufficiently complex means "anything that includes addition and multiplication of natural numbers".

An AI may be able to prove that sum(range(1, n+1)) == n*(n+1)//2 for all natural numbers n; that is, it may output a string that's a valid proof. Smart ones can, dumb ones can't. Just like humans. Intelligence is what limits you.

But if a set of axioms and inference rules don't allow for a proof of a given theorem T, no matter how smart you are, even if your silicon brain is smarter than all of mankind, monkeykind and birdkind added up, you can't transcend any limitation that's found wholly outside your intelligence. As in this case, where it's the nature of the mathematics you've made that prevents T from being proven, and not your inability to find the proof.

Similarly, if we agree that no evidence or reasoning can prove or disprove the existence of god, then no AI can know whether god exists: it's not your knowledge or ability to reason that limits you, it's the nature of knowledge and reasoning itself.

Looked upon that way, Gödel's theorem doesn't say anything about AI. It says something about the world.

I don't know what a "perfect" intelligence is. One that can solve all NP problems in O(1) time and space? Or s/NP/Recursive/? Or just something that can solve all recursive problems in finite time? To implement that, all we lack is the ability to store unbounded information in a world of finitely many atoms. Can intelligence do something more than Turing machines? Does that mean the answer is no? Or that we need to connect nerves to the PCI bus?

Re:godelstheorem?

[Sparr0]

Of course you can prove a negative, usually by contradiction. Assume the opposite and see if that produces a contradiction. If it does, then the original negative is true.