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?
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?
Equine Mammals Are Considerably Smaller
One long-term dream is to have formal proofs of all of the central theorems in mathematics
And what theorems would *those* proofs be based on?
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)
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?
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?
But can you prove it computationally?
Blog
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?
Unfortunately his presidency will either be incomplete or inconsistent.
And then there are leaders out there like Castro, who doesn't seem to halt.
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
Godel's Theorem has to be the most misunderstood statement of all time. I won't attempt a statement here because, right or wrong, I will get 10 incorrect corrections, maybe one correct one. There's kind of a mini Godwin's law in effect for any discussion here about something with the words "automated" and "theorem" in the title. Inevitably it will devolve into bickering about Godel's Theorem, even though it *plays no role at all in what these projects are trying to accomplish*. They merely want to record a giant database of theorems and proofs, to aid in finding further theorems and proofs. Even without Godel's Theorem, since there are infinitely provable statements, the list would never be complete anyways.
It is nothing but BS that the computer is better than human. Not to mention profound stupidity to think that the computer is infallible i.e. it is programmed by humans.
I read the first bit of Freek Wiedijk's article and it's political nonsense. All they've done is use the word "formalization" to describe the process of encoding mathematics "in the computer". What this does is hijack the common notion of formalization for use for there own purposes. Because, formalization is good, right? Well, not if you read and really understand what it does, and infinitely more important, does NOT mean in this context.
Point of fact, using computers does NOT take human minds out of the equation. It just hides them giving people the illusion of a more effective system.
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?
The question of whether or not God exists is pure sophistry. A sufficiently intelligent agent would pay it no more heed than the question, "Do concepts live in barns?"
Similarly, Godel's theorems are often portrayed in sophist manner. They prove interesting and perhaps surprising facts about mathematics, but they don't say anything remotely close to "some truth is unknowable".
I meant "inconsistency and incompleteness are not mutually exclusive".
On the contrary, they often go hand-in-hand.
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?
On average, a programmer introduces 1.5 bugs per line while typing.
That's quite wrong, a better estimate is that, on average, a programmer introduces from 1.5 up to 5 bugs per 100 lines while typing.
A bug in a paper about bugs... quite fitting.
And that's despite 638 attempts at forced termination.
One swallow does not a fellatrix make
It seems to me that there's this revolutionary new religion out there, called Judaism, that has a creation myth that better describes a soul. Then there's this offshoot cult of Judaism, that takes it a step farther... so let me try to explain.
When (in the creation myth) Adam eats the fruit, having been told "the day you eat the apple, you die", he begins to die. That is, his body starts to fall apart. But as his body falls apart, his soul -- tied to his body -- starts to fall apart, too.
So when Adam completely dies and his body disintegrates, his soul has also basically disintegrates. That's why, in Judaism, they have such things as the statement "The dead do not praise God" (Hezekiah, also the psalms, also ecclesiastes).
And Judaism basically leaves it at that. So when you saw your grandmother's body and soul disintegrating, that's basically what you were seeing.
But the Christian cult of Judaism takes it a bit farther, for through a good deal of evidence and analysis, they the creator-being who created Adam (and all of us) as being identical with the spirit of Love. But even Love cannot love what does not exist. So the death and disintegration are a denial of the power of that Love.
Yet this creator being is also identified as being all-powerful. So they understand that certain events about 2000 years ago, in which the entropy of death and disintegration are set reverse, are this creator being simply exerting His power as He would be expected to do.
Which is a very revolutionary idea, that entropy can be reversed, especially considering that all our physics and even mathematics does not imply that it can be. On the other hand, our physicists and scientists have not been able to observe a creation event, which explains why they are trying to get CERN going (not realizing that if they did trigger a creation event, they still would not be able to observe it). But it should be observed that arguably a creation event is itself a reversal of complete entropy. So our 2nd law of thermodynamics, while completely valid in the frame of reference of our universe, probably is not universally valid.
Correct Horse Battery Staple: 72 bits of entropy. Enter "Correct H" into google. When it generates the phrase, that's
Well, the list of theorems for which informal proofs have been presented is finite. The goal of this project is to formalize those proofs so they can be verified by proof checkers rather than to prove random facts.
Actually even if we just limit the Central Theorems to "a mathematical statement that has been claimed to be true", then we still have a finite list. (and there is little need to prove a statement true if nobody cares whether it is true or not)