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."
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.
How we know is more important than what we know.
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.
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?
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.
If I can be modded down for being a troll, can I be modded up for being an orc, or a balrog?
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.
No problem is insoluble in all conceivable circumstances.
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?
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.