There's one other interesting application of APC: It provides a secondary path to legitimacy for people who can't get through the primary one. DeBranges had a wrong proof of the X conjecture. A decade later, he found a very long right proof, but couldn't get anyone to look at it. [Eventually he found someone to go through it, and the reader was able to recommend the proof to others.] An APC would let John Brillhart reply to a purported prover of FLT: "Your proof is complex and I don't have time to follow it all the way through. But if you can get it through the APC at math.foo.edu/~apc, people will believe it works." The APC folks claim to have built up enough machinery to have proved the prime number theorem from the axioms. This seems to me to settle the question "Is it possible to formalize math sufficiently to trace it back to axioms?" There's a part of math that isn't about theorems, but a lot *is* theorems and other kinds of calculations. Wrt checking Mersenne primes: Most of the computing is used in checking and rejecting the millions of composites. There are 40+ MPs known. The check time for an individual test is a few months on a PC, or a few weeks on high-powered hardware. The Lucas-Lehmer test depends on the factorization of MP+1, which is easy because it's a large power of 2. (Pratt used a well-known P-1 test.) As far as anyone knows, the LL test is the most efficient check. The GIMPS crowd does double checks on their rejections, and the successes are triple checked on different hardware with different programs by different people. That's about the same level of assurance expected from an APC. Rich -----Original Message----- From: math-fun-bounces+rschroe=sandia.gov@mailman.xmission.com on behalf of dasimov@earthlink.net Sent: Fri 3/3/2006 12:04 PM To: math-fun Subject: Re: [math-fun] Most influential mathematician? 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. _______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun