Slashdot Mirror
Are Computers Ready to Create Mathematical Proofs?
DoraLives writes "Interesting article in the New York Times regarding the quandary mathematicians are now finding themselves in. In a lovely irony reminiscent of the torture, in days of yore, that students were put through when it came to using, or not using, newfangled calculators in class, the Big Guys are now wrestling with a very similar issue regarding computers: 'Can we trust the darned things?' 'Can we know what we know?' Fascinating stuff."
The headline does a slight disservice in describing the article that way: Whether or not computers can create proofs isn't an issue. The problem comes when the resulting proof is too involved to be verified by a human, and so the computer's work has to be trusted.
I mean, we've used computers to prove much of boolean and linear algebra. The most famed result in the field is that of the Robbins Conjecture, proven entirely by computer. The computer produced a very "inhuman" proof...
and there are already programs out that help with this. Here's one for example...
It's not hard to *see*. It's hard to *prove*. Very little of mathematics is consumed with proving deep, mystical statements that no one would ever anticipate to be true. Much (maybe most) of mathematics is built around proving (relatively) obvious things. Why bother? because sometimes, relatively obvious things turn out to be false, and there's no way to know that they won't until you've prooved them true. In general, showing that discrete (or semi-discrete) phenomena are optimal is fairly tricky; you can't just appeal to calculus to optimize some function. You often have to somehow break the search space up into a bunch of disjunct cases that span all the possibilities, and be able to prove that they span all possibilities. Then, if you're lucky, you can use some kind of calculus-type argument on the continuous spaces you're left with.
Theorem provers have been around for a long time. A net search should turn up a ton of hits. The key is to implement a system that can be verified by hand, and then build on it.
(S(SKK)(SKK))(S(SKK)(SKK))
http://www.nytimes.com/2004/04/06/science/06MATH.h tml regfree link
What if the stack is very large, for instance? Is it still obvious that the pyramid is best? Consider a similar problem, that of packing squares in a rectangle. When the rectangle is small, it is obvious that the best way is to pack them together starting from one corner, leaving a little wastage on the opposite two sides. It seems strange, but it is true, that when the recangle is very large, this strategy is not optimal. More squares can be packed when they are not packed in such a regular pattern. This is the main difficulty with proofs of this type. It can be easy to prove that a given strategy is not optimal, but not so simple to show that no better strategy can exist.
I professor showed me the Robbins Algebra proof a while ago. I was going to link here, but first I searched the page for (Score:5, Informative), and there you were :)
Here's an excerpt:
In 1933, E. V. Huntington presented [1,2] the following basis for Boolean algebra:
x + y = y + x. [commutativity]
(x + y) + z = x + (y + z). [associativity]
n(n(x) + y) + n(n(x) + n(y)) = x. [Huntington equation]
Shortly thereafter, Herbert Robbins conjectured that the Huntington equation can be replaced with a simpler one [5]:
n(n(x + y) + n(x + n(y))) = x. [Robbins equation]
Robbins and Huntington could not find a proof. The theorem was proved automatically by EQP, a theorem proving program developed at Argonne National Laboratory.
PUBLIC SPLIT ON WHETHER BUSH IS A DIVIDER -CNN scrolling banner, 10/15/2004
Actually, this is three of the four quadrants of knowledge...
KK | KD
___|____
|
DK | DD
So, you can:
Know that you Know something
Know that you Don't Know something (the second most common)
Don't Know that you Don't Know something (most things fall in this category for most people)
Don't Know that you Know something (the most interesting of the categories)
Big, huge, red tape operations can easily fall into the latter category (DK)... since it is rather easy for a group to obtain knowledge, yet be unaware of it [political commentary omitted].
"It's tough to be bilingual when you get hit in the head."
Here's a link to the Flyspeck Project, briefly mentioned at the end of the article, which aims to give a formal proof of the theorem.
At least some provable properties can be "pushed" through the compilation process all the way to the resulting object code. If you're interested, you can look into proof-carrying code and typed assembly language (papers by Necula, Appel, Walker, Zdanzewic, Crary and a cast of thousands.)
The resulting proofs are still hairy enough that they have to be checked by machine, but the size and complexity of the proof-checker is much less than that of the compilation toolchain. That means that while there's still some code that has to be trusted, it's much less. Here's my informal scariness hierarchy:
Normal model (you have to trust everything) > type safe languages (you have to trust the compilers / interpreters) > proof-carrying code (you have to trust the proof-checker*).
If you haven't already, you should definitely read Ken Thompson's Turing Award lecture, "Reflections on Trusting Trust" here.
* - Pedantry point: If you're talking about Necula's original PCC work, you also have to trust the verification condition generator, which is some fairly deep voodoo. Appel's Foundational PCC addresses this to a signficant extent.
Some things have to be taken as Axioms. A=A is one of them. All the things you prove that rely on A always being equal to A can be taken as true PROVIDING you accept that axiom. We like to pick axioms that we have a gut feel 'must' be true - but you can do interesting mathematics by denying some of those axioms and see where they take you. The classic geometric case of denying that parallel lines never meet produced a whole range of interesting geometries that don't exactly represent the real world but none-the-less have interesting and useful consequences.
So - when you come across a theorem that you can't prove but are pretty damned certain is true - you COULD choose to simply make it be an axiom. The problem is that the theorems you are subsequently able to come up with are only as reliable as your initial assumption of that axiom.
If your axioms eventually turn out not to match the real world - then all you have is a pile of more or less useless theorems that don't mean anything for the real world.
It's therefore pretty important to stick with a really basic set of axioms to reduce the risk that an axiom might turn out not to be 'true' for the real world and bring down the entire edifice of mathematics along with it.
If we ever found some sense in which A!=A then every single thing we thought we knew about math would be in doubt.
www.sjbaker.org
The people at the Risc Institute are creating cool stuff like Theorema, which helps in automatically proofing things. Some of these people teach math at a university in Hagenberg where I got the chance to see this thing in action, it is really amazing how well this works.
Open Source Alternatives
I believe its called the fallacy of the false delemma.
He who knows not and knows he knows not is a wise man. He who knows not and knows not he knows not is a fool.