March 2006 - mathfun@mailman.xmission.com

Re: [math-fun] Proof checking and program checking
by The Purple Streak, Hilarie Orman 06 Mar '06

06 Mar '06

I did a little of this stuff many years ago, mainly for software verification. The surprising thing is that many errors are caught during the process of preparing the material for verification, and almost none are caught during verification. This latter arises either because the specification is wrong in some respect (e.g., doesn't capture the concept precisely) or because the verification system is faulty, or because there aren't any errors left (hah!). At the time, there seemed to be general agreement that the process of specifying and verifying things (theorems, software, hardware) was valuable, but it was also extremely expensive and required a new class of experts. Automated theorem verification could become a new mathematical specialty, generating its own kind of complexity theorems and great unsolved problems. Hilarie

3 2

[math-fun] Re: a(n) = trace(B(A^n))
by Joerg Arndt 05 Mar '06

05 Mar '06

* Edwin Clark <eclark(a)math.usf.edu> [Mar 04. 2006 22:55]: > > In discussing Creighton Dement's floretion generated > sequences with him I came across the following fact: > > Every sequence a(n) defined by a k-th order linear recurrence > with constant coefficients over any commutative ring with identity > can be realized in the form > > a(n) = trace(B(A^n)) > > where A and B are k x k matrices over the ring in question. > > Surely this must be known! Can someone provide a reference? > > [Taking A to be the companion matrix of the polynomial defining > the recurrence will clearly give a sequence satisfying > a recurrence relation of order k with the desired coefficients > then one just needs to fiddle with B to get the desired initial > terms. One can take all entries of B to be 0 except for the > last column and it is not too hard to find a formula for the > last column of B in terms of the coefficients and initial > conditions.] > > --Edwin Note that practical computations can be much accelerated via computations modulo the polynomial (cf. p.463 of the fxtbook, http://www.jjj.de/fxt/fxtpage.html#fxtbook ). I'd very much appreciate a reference for that one, too (found it myself). jj

1 0

[math-fun] Re: proofs
by James Propp 04 Mar '06

04 Mar '06

>Anyone is free to include in their math paper >a statement of the shape "Computer checkable proofs >of Theorems 1 and 2, and Lemmas 3-6, are available >at the URL math.foo.edu/~baker/paper7.txt" . >Maybe noone has thought to do it yet. Doron Zeilberger does exactly this in many of his articles. Jim Propp

2 1

[math-fun] Word replacement, not for the better
by Steve Gray 04 Mar '06

04 Mar '06

Does anyone know why the nice word "factoring" was recently (?) replaced in the U.S. by the ugly word "factorizing?" Continuing this trend, the word "factor" should also be replaced, perhaps by "factorizer" or "factolets" or "factoreenies." Or, combining "factor" and "atom," they could be called "fatoms." Steve Gray

3 2

Re: [math-fun] Most influential mathematician?
by dasimov＠earthlink.net 04 Mar '06

04 Mar '06

franklin writes: << >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. >> Well, after being a mathematician for 34 years, I believe I do. Well, I believe I mentioned the hardest parts to such a project in the part of my post that you didn't quote. Obviously, if the proof being checked uses another theorem, then that theorem would have to have a seal of approval, itself. And once any theorem has been rigorously checked, and perhaps re-checked to be on the safe side, it could be adoped as an "axiom" forever after in this scheme. At first, a very large number of well-accepted and time-tested theorems would be grandfathered in -- as temporary axioms. Eventually, perhaps such a project would get around to fully checking old theorems as well. >> 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. >> --Dan

1 0

Re: [math-fun] Most influential mathematician?
by Henry Baker 03 Mar '06

03 Mar '06

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(a)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

2 2

Re: [math-fun] Most influential mathematician?
by dasimov＠earthlink.net 03 Mar '06

03 Mar '06

P.S. Automated proof-checking may become an important issue in the future, now that we've seen at least one proof (Hales's computer portion of his proof of the Kepler conjecture) that has overwhelmed our combined computer and especially human resources. But as far as I know that is the only example so far; for all but measure zero among putative proofs, the old-fashioned system of peer-checking has worked well. (Aside to Steve: the Monthly is not included, since imo the outgoing Editor has taken an idiosyncratic view of the Editor's duties.) There are some examples of proofs erroneously believed valid for many years (e.g., Kempe's wrong proof of the four-color theorem (11 years), and Dulac's wrong proof of part of Hilbert's 16th problem* (58 years). But I've heard of only a handful of such examples. --Dan _____________________________________________________________________ * This is the conjecture that if a vector field in the plane is defined by real polynomials in x and y -- V(x,y) = (P(x,y), Q(x,y)) -- then its trajectories include only a finite number of limit cycles. It was finally proved in 1981 by Ilyashenko -- or so it is believed.

3 2

Re: [math-fun] Most influential mathematician?
by dasimov＠earthlink.net 03 Mar '06

03 Mar '06

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

3 2

RE: [math-fun] Most influential mathematician?
by Pacher Christoph 03 Mar '06

03 Mar '06

>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? this reminds me to the halting-problem, which is known to be not solveable... --Chris

2 1

Re: [math-fun] proofs; sudoku
by Henry Baker 03 Mar '06

03 Mar '06

I agree that the vast majority of math is built on firm foundations, as is the vast majority of most other fields. However, as is sometimes the case, a correct result may have an incorrect proof, so the proof of the pudding may not always be in the eating :-). While there are certainly problems for which the proof is as long as the search for the proof, there currently (at least until P=NP) appear to be problems for which the proof is considerably shorter than the search tree. Re Mersenne Primes, Rich would know better than me whether there exist shorter proofs of primehood for these particular primes than the program which find them. Vaughan Pratt showed a while ago that all primes have a relatively succinct proof, but finding that proof requires (as I recall) the factorization of p-1 & lots of other factorizations. Proving a number composite is (currently) very cheap compared with finding the factors in the first place. At 06:43 PM 3/2/2006, Schroeppel, Richard wrote: >An extreme endpoint of checking is verifying a Mersenne >Prime, where you pretty much have to repeat the LL test. >But of course they do that anyway. > >A checkable proof of the Odd Order Theorem could be >very useful, since it would likely result in the discovery >and repair of some minor errors. > >But it seems unlikely that much of our edifice is built >on wrong stuff, so making checks required seems extreme. >And it could chase the non-detail-oriented out of the >profession. (Or perhaps they'd make their grad students >do it. Hmmm. Would the 8th Amendment apply?)

1 0