Slashdot Mirror
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."
Why is this tagged "godelstheorem"? It's not like incompleteness magically applies only to electronic computers, as opposed to meatbags...
"They were pure niggers." – Noam Chomsky
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?
Give me Classic Slashdot or give me death!
Do you really need supercomputers in all practical cases?
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)
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.
That Gödel's Completeness Theorem for first-order logic--predicates, individuals, quantifiers ("for all," "exists"), and truth connectives (not, or, and).
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.
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.
Are you adequate?
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.
Are you adequate?
Knowing a little bit about formal proofs and a fair bit about programming, but nothing about the computerized verification or generation of formal proofs, I really doubt the FPU is used for this stuff.
In Capitalist America, bank robs you!
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?
"I object to doing things that computers can do." -- Olin Shivers, lispers.org
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.
Find free books.
That needs a couple of small amendments:
Intuitively, your algorithm fails if the theory admits of contingent statements (as first-order logic does), or if the theory is incomplete (as arithmetic is). If you feed it a contingent statement, it will never terminate, since no proof will have either the statement or its negation as its conclusion. Same goes if your theory is incomplete and you feed it one of its Gödel sentences.
If you can prove that for every statement in the language, your axiomatic theory has a proof either of that statement or its negation, then your algorithm works for that theory. (The textbook I used calls such theories syntactically complete, but books often use just "complete" for this property, which is different from Gödel's "(in)completeness"...)
(All of the above assumes the axiomatic theory is sound to start with, i.e., there are no proofs of invalid statements. If your theory is unsound, you've got bigger problems.)
Are you adequate?
Penrose, Hofstadter and you all share a basic assumption: that there exists a "real" property that the word "intelligence" denotes. I think that assumption is flawed.
The alternative view is that "intelligence" is just a term in a cultural classificatory scheme. This implies several things:
Basically, arguments about whether machines can "think" are cosmological arguments; what's really at stake is not what machines can do, but rather, our ideas of what the world is, what people are, and how people relate to the rest of the world; in particular, the relationship between people and machines.
So now we come at my personal, half-serious test for machine intelligence: can I bring a civil lawsuit against a computer, or the state press criminal charges against it? More generally: can a machine have responsibilities in the same sense that a person does?
The first point of this is that the most fundamental gulf between people and machines isn't a physical or a cognitive gulf: it's a social gulf. Whether a machine has responsibilities isn't determined by any property intrinsic to the machine itself; it's determined by how people actually relate to the machine. Intrinsic properties of the machine aren't irrelevant, but they're neither necessary nor sufficient.
The other point is to highlight that the word "intelligence" in AI is being used in a technical and artificially narrow, purely cognitive sense, that doesn't reflect the whole range of implications that the word has in our culture. If we take the broader view, "intelligence" isn't just about cognition; it's at least as much about moral agency. We can turn the whole machine intelligence issue on its head by suggesting that we don't call humans "intelligent" because we catalogued their intrinsic cognitive faculties and found that they met an independent criterion of "intelligence"; rather, we call them "intelligent" because we regard them as moral agents, and from that assumption, it follows that they are are intelligent. Then, the reason we don't regard machines as intelligent is simply that we don't regard them as moral agents.
Are you adequate?