On 9/28/07, Henry Baker <hbaker1@pipeline.com> wrote:
I guess there's also another meaning of "Far Side", as in the "Far Side" cartoons...
I know that Mann is trying to be "open ended", but his topics seem to me to be a bit fuzzier than Hilbert's topics.
I don't know if (D)ARPA is interested, but the time is right for the following project, which could conceivably take 10 or more years:
--- Mathpedia/Wikiproof/(still looking for a good name):
Computers are now ubiquitous, and now have enough memory & processing power to enable the following scenario for mathematics publishing:
In order to get a paper published, you have to make all of the proofs mechanically checkable, and submit them to a web-based proof checker prior to being considered by the referees. No proof; no publish. This is arXiv with a prerequisite.
I wonder why you think this project would be worth the huge diversion of effort it would involve. Number theorists would have to devote effort currently devoted to advances in number theory to work on formalization of existing work. Algebraic geometers would have to devote effort currently devoted to advances in Algebraic geometry to work on formalization of existing work. And so forth. Why is formalization so important that work in every other field of mathematics should be slowed to make progress in formalization? The main advantage I see in formalization is that incorrect proofs are not mistakenly accepted by the mathematical community. But this seems to be a solution in seach of a problem; I can count on the fingers of one hand the cases I know of where a widely accepted result turned out to be incorrect. It's true that under the current system, once an important work is published, other mathematicians devote effort to verifying its correctness. But this work would not be eliminated; its main purpose is not the catching of errors, but the achievement by the verifier of a deeper understanding of the result and its proof. -- Andy.Latto@pobox.com