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?

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

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.

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.