- mathfun@mailman.xmission.com - mailman.xmission.com

[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 03 Mar '06

03 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

[math-fun] a mathematician under the influence
by James Propp 02 Mar '06

02 Mar '06

If we refine the question to something like "Who would be most successful in leading a campaign to automate proof-checking in huge swaths of mathematics?", then I'll start the bidding by nominating David Mumford. His experience as an algebraic geometer makes him eminently qualified to assess just how deep mathematics can get, and his more recent work with computer vision makes him credible as an authority on what current methods of automation might be able to achieve. Don Knuth would also be plausible as the leader of such a automation crusade. As a computer scientist, he has a keen understanding of what it takes to create a software system. And, to the extent that his personal style and his sense of design contributed to the success of TeX, one might predict that he'd use the same flair to develop and promote a general- purpose proof-verification system for mathematicians. If the impulse behind the question is "Who's the one person in the world such that, if I convince him, he'll convince everyone else?", there's a catch: It could be that the more qualified someone is to say "This is something we mathematicians can and should do" and get people to take notice --- that is, the more knowledgeable he/she is about what math is, and what early 21st century computers can do --- the less likely it is that he/she would say it. Jim Propp

1 0

RE: [math-fun] Most influential mathematician?
by Jud McCranie 02 Mar '06

02 Mar '06

I think Clifford Pickover solicited nominees for this several years ago. Anyone remember?

1 0

[math-fun] Influential mathematicians
by Steve Gray 02 Mar '06

02 Mar '06

The majority of the much less than 1% of the general public who has heard of any contemporary mathematician would probably name Andrew Wiles. Of course we're probably not talking about a popularity contest, but if we were, J.H. Conway's name would also come up. I wouldn't include those like Gardner who are mostly popularizers, as valuable as they are. Steve Gray

1 0