Re: [math-fun] Most influential mathematician?
Dan: What you are describing is the whole Hilbert/Russell program, which was derailed to some extent by Goedel. However, the absence of a finite set of axioms for mathematics doesn't mean the end of proper proofs. Look how much math today depends upon the Riemann Hypothesis, the Axiom of Choice, etc. Unfortunately, we don't even have a proper proof-checker for high school plane geometry (that in itself would be a good thing, so that high school students could check their own work). (High school plane geometry is decidable, as it is reducible to the theory of Real Closed Fields, but the general decision process is multiply-exponential, and hence currently not practical. But a decision procedure isn't necessary to verify a proof -- only to find one.) At 10:15 AM 3/3/2006, dasimov@earthlink.net wrote:
Gene wrote re proof-checking software:
<< Such a computer program would be as intricate as the proofs it is expected to verify, and is subject to the same human error. There cannot be certainty of correctness of a proof without certainty of the correctness of the proof-checking software. Could the program check itself?
It seems possible there could be a bootstrap method to create perfect proof-checking software (I suspect this has already been done for plane geometry), but in general this would rely on the mathematics in question having been axiomatized. Axiomatizing all of math is one of the biggest obstacles to having a universal proof-checker lies. The other is translating putative math proofs, often written largely in natural language, into putative symbolic proofs.
If a putative proof is then put into official proof format, as defined by logicians, then -- assuming sufficient computing resources -- checking it should be a piece of cake. (Each statement in sequence must be either
1) an axiom or
2) a statement B such that statements A, and A => B, are prior statements in the proof,
and the last statement is what was to be proved.)
There is also the question of the consistency of the axioms, and imo especially those of set theory/category theory. E.g., since there can't be a set of all sets, I have to question the meaning of the "class of all sets" -- a "concept" that is dubious at best.
--Dan
On Friday 03 March 2006 18:49, Henry Baker wrote:
(High school plane geometry is decidable, as it is reducible to the theory of Real Closed Fields, but the general decision process is multiply-exponential, and hence currently not practical. But a decision procedure isn't necessary to verify a proof -- only to find one.)
Are you sure? I think I remember reading (several years ago) a book that purported to describe a practically usable algorithm for finding proofs of problems in high-school plane geometry, and that claimed it was already being used to good effect by Chinese participants in the International Mathematical Olympiads. Am I misremembering? Aha, the following is about the same method: http://www.mmrc.iss.ac.cn/~xgao/paper/ieee-logic.pdf and it doesn't in fact purport to prove everything that can be proved in that domain. It's still pretty impressive, and likely to appeal to many munsters. (Was that the right term?) -- g
Very interesting paper, thanks! This paper brings up an important issue, which is already familiar to those in the symbolic algebra field -- the mechanical version of the proof can be (and probably usually is) completely alien & incomprehensible to a human. Thus, although the proof can be checked and rechecked, it could still be completely opaque for human readers. This isn't to say that a human-understandable proof can't be checked by a computer -- that would be my goal. It's just that a decision procedure might produce a non-human ("inhuman" ?) proof. At 12:22 PM 3/3/2006, Gareth McCaughan wrote:
On Friday 03 March 2006 18:49, Henry Baker wrote:
(High school plane geometry is decidable, as it is reducible to the theory of Real Closed Fields, but the general decision process is multiply-exponential, and hence currently not practical. But a decision procedure isn't necessary to verify a proof -- only to find one.)
Are you sure? I think I remember reading (several years ago) a book that purported to describe a practically usable algorithm for finding proofs of problems in high-school plane geometry, and that claimed it was already being used to good effect by Chinese participants in the International Mathematical Olympiads. Am I misremembering?
Aha, the following is about the same method:
http://www.mmrc.iss.ac.cn/~xgao/paper/ieee-logic.pdf
and it doesn't in fact purport to prove everything that can be proved in that domain. It's still pretty impressive, and likely to appeal to many munsters. (Was that the right term?)
-- g
participants (2)
-
Gareth McCaughan -
Henry Baker