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

godelstheorem?

[retchdog]

Why is this tagged "godelstheorem"? It's not like incompleteness magically applies only to electronic computers, as opposed to meatbags...

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

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

Re:godelstheorem?

[Anonymous Coward]

Isn't non-artificial intelligence necessarily incomplete as well? It's not like the brain has a sprinkling of magic pixie dust that computers can never have.

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?

[Jane Q. Public]

My understanding was that Gödel proved that S could not contain itself, which was the downfall of that very argument. Consider a statement about S: "S contains all possible propositions." That proposition may be true, but it is not possible to prove that proposition within S, so S is incomplete. Q.E.D.

That is a brief summary but even if I misunderstood that, a proven incompleteness by itself still does not prove consistency. They are not mutually exclusive.

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.

Re:godelstheorem?

[CTachyon]

Actually, there is a 'higher intelligence' giving human beings thoughts as you put it (i.e., souls). You don't have to start with this assumption though as the implications of Godel's theorems would lead you to that conclusion if you start with them (and the theorems are pretty rock solid).

Bullshit. The only thing Gödel's incompleteness theorems prove is that no knowledge, not even human knowledge or even a deity's knowledge, can be both consistent and complete. Human beings are so ridiculously inconsistent that completeness doesn't even enter into the picture and Gödel doesn't apply.

Alzheimer's is proof by counterexample that souls don't exist. Ever had a relative die of Alzheimer's? My grandmother died of the fast-acting, early-onset form. She was symptomatic in her late 40s and was barely 50 when she was diagnosed. Within 5 years she was behaving like a hypersexed sullen teenager, after 7 years she completely lost the ability to speak a grammatically correct sentence, and 9 years in she died as a bedridden zombie incapable of chewing and swallowing her own food. Her "soul" died piece by piece before my family's eyes, leaving first a wild animal with the power of speech (in the form of babble), and then only an empty husk of a body. The "soul" is divisible, and physical disease can kill it piecemeal by attacking the brain. Therefore, the "soul" is a physical part of the brain. And as flawed as that "proof" is, it's more proof than you offer for your baseless assertions about Gödel's incompleteness theorems.

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:Answer me this...

[colmore]

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.

Re:The exact opposite is true

[lexDysic]

If it's possible to enumerate all valid proofs I propose the following proving algorithm: Run through all valid proofs; once you get to a proof whose conclusion is the theorem you want to prove, return that proof.

[if you don't know whether your theorem is true or not, run the above algorithm on its negation as well].

What's wrong with my algorithm?

The problem is that some propositions P have the following two properties:

1: P has no proof
2: (not P) has no proof.

So your algorithm searches forever and you don't know if it just hasn't found anything yet, or if there is nothing to be found.

No, it doesn't work.

[Estanislao Mart�nez]

If it's possible to enumerate all valid proofs I propose the following proving algorithm: Run through all valid proofs; once you get to a proof whose conclusion is the theorem you want to prove, return that proof. [if you don't know whether your theorem is true or not, run the above algorithm on its negation as well].

That needs a couple of small amendments:

1. You shouldn't run the algorithm on the statement and its negation in sequence, because the basic algorithm will never terminate for an unprovable statement. To harden the algorithm, you should interleave the runs for the statement and its negation: as you enumerate each valid proof, you check whether the conclusion is either your statement or its negation.
2. Strictly speaking, what's relevant here is not the "truth" of a statement, but rather its validity given the axiomatic theory. A valid statement is one that is true under all interpretations of the theory; an invalid statement is false under all interpretations of the theory; a contingent statement is one that's neither valid nor invalid, since it's true under some interpretations of the theory and false under others.

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

The whole discussion is flawed.

[Estanislao Mart�nez]

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:

1. There isn't really a set of necessary and sufficient conditions for something to be "intelligent." What the various uses of the word share is a set of family resemblances.
2. The classification is tied to a bunch of cultural practices. In the case of "intelligence," it's easy to come up with alternatives: the distribution and specialization of labor, and the assignment of rights and responsibilities. In the first case, we give certain jobs to people who are "intelligent," while giving others to people who are "not intelligent"; in the second, we assign the full range of civil rights and responsibilities to people who have a fully developed "intelligence," but deny rights to, and excuse from responsibilities, people whose "intelligence" is lacking (children, defense of insanity).
3. The term, therefore, is culturally variable and historically contingent. A hundred years ago, it was common opinion among educated westerners that women, children and non-whites were not "intelligent" and did not "think," often with specialized technical vocabulary for explaining the cognitive faculties of "non-intelligent" humans. Today people have seemingly serious arguments about whether a computer can be "intelligent." What happened during that time? Universal suffrage, decolonization, the rise and fall of behaviorist psychology, the rise of cognitive science, increasing secularization of culture, etc. (The derogation of women's and minorities' cognition does continue, however, but expressed in newer terms: instead of saying that women and negroes experience "henids" instead of "thinking in ideas," people today say that women or African-Americans on average have lower IQ than white men, and that IQ is subject to significant inheritance (see Lawrence Summers or The Bell Curve)).

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.

Perhaps you misunderstand what a soul is.

[MickLinux]

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.