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."
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?
Of course this applies. No, Gödel's theorem doesn't just apply to computers, but it does apply too!
And it is actually a very relevant point. Since Gödel proved that a formal system must be either incomplete or inconsistent -- and we do not really know which one applies to mathematics -- it may be that a "central" theorem of mathematics will contradict some other finding, later, which turns out to be equally central.
Not very likely, but who knows?
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
can human brain be simulated by a Turing machine? It's plausible that human brain obey physics - but is physics Turing computable?
Of course we can create physical machines that's the same as human brains - million of of them everyday:)
Let's take a step back and not worry about abstract reasoning for a moment. Here's a concrete example with a very simple function. You really should try to solve this before talking about using "clever checking", etc.
(Hint: Nobody knows if it always halts or not. My apologies if you get hooked on this problem too...)
One might argue that the brain is merely a biological computer not fully understood.
Or, perhaps, humans could be nondeterministic and therefore not computers at all.
Again, restrict the problem space to what is feasible. This pathological example is one of infinite complexity that is impossible in practice (int cannot be substituted for an infinite precision integer). There will be overflow or there will be a state where n is the same as a state before after a finite number of steps (there are only a finite number of possible values for n). So this program will conditionally halt for different values of n (of which there is a finite number).
I was talking about applying theory to something that is possible. Obviously you can set up a simple system which is impossible to execute and generate an infinite space of inputs and outputs. This is plain cheating in reality, often the mistaken realm of application of the halting problem.
FYI: The function above can be easily expressed as a 3-symbol, 6-state Turing machine where only 3 of those states do the main algorithm and one of the states is just to catch the halting condition.
Turing machines that aren't allowed to have infinite tapes are called finite state machines. FSMs are worthlessly boring. Turing machines are interesting because of the possibility of infinite state.
As for your point about an infinite precision integers: yeah sure, but they can be implemented as strings, and we have TB hard drives now! Have you bothered to consider how large 2^(1,000,000,000,000) is? (Hint: There are only ~2^265 atoms in the known universe.)
Well this is a decent point. It's impossible to create a truely random number generator in software but you can create one in hardware which, for example, measures the decay of radioactive particals or some such.
But in that case it still doesn't mean AI is impossible, something is still artificial even if some of it's capabilities have to be instituted in hardware rather than software.
While computers are nothing more than finite state machines (with an insane amount of states), their theoretical base can be found in Turing Machines and.... those come in a non deterministic flavour. Take note at the "Equivalence with DTMs" sections.
So, if the human brain works non-deterministically, it can be simulated by a deterministic "brain". If this doesn't require infinite amount of states (considering what we know of the universe, this most likely won't be the case), it can thus be simulated again with a finite-state machine with an insane amount of states. That is exactly what a computer is, as I said before.
Throwing around "non-deterministic" won't save you. It might be something else that sets apart the human brain, but it won't be its non-deterministic nature.