Re: [math-fun] Most influential mathematician?
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
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.)
Do you have any idea how far published mathematical proofs are from this level? I would guess that a typical published proof would require millions or even billions of statements. So any such project would have to operate at a higher level than that. And now you come to another problem: groundbreaking results, and a large fraction of those that aren't groundbreaking, involve the introduction of one or more new ideas. And those ideas would have to be introduced to the proof machinery before it could verify the result - at which point the utility of the exercise is very much in question. ___________________________________________________ Try the New Netscape Mail Today! Virtually Spam-Free | More Storage | Import Your Contact List http://mail.netscape.com
This is a large project, because the amount of infrastructure that it needs is enormous. Just like the development of a large SW system like MS Windows involves a huge number of sub-parts, the infrastructure of a mathematics system would involve tens of thousands, if not hundreds of thousands of lemmas & theorems. Bob Boyer tells me that even the current successes of proof checkers involve thousands of lemmas. One of the tasks of such a project would be to name/index all of the lemmas in mathematics (in a manner similar to the naming/indexing of all Integer Sequences). As some have already speculated, this task involves the formalization of all known math -- a huge undertaking. Once such a framework exists, the amount of additional machinery for a new theorem would be (more-or-less) proportional to the size of the English/French/whatever paper convering the same material. (An analogy is the implementation of a standard -- e.g., MPEG4. The size of the SW to implement the standard is typically proportional to the size of the published standard in English. Of course, this depends upon the existence of large subroutine/function libraries to implement common algorithms not spelled out in the standard.) At 11:12 AM 3/3/2006, franktaw@netscape.net wrote:
Do you have any idea how far published mathematical proofs are from this level? I would guess that a typical published proof would require millions or even billions of statements.
So any such project would have to operate at a higher level than that. And now you come to another problem: groundbreaking results, and a large fraction of those that aren't groundbreaking, involve the introduction of one or more new ideas. And those ideas would have to be introduced to the proof machinery before it could verify the result - at which point the utility of the exercise is very much in question.
participants (3)
-
dasimov＠earthlink.net -
franktaw＠netscape.net -
Henry Baker