I think that the bulk of the initial part of this work would be done by computer scientists & logicians. Only later, when the bulk of the existing math needs to be shoveled in, would mathematicians be more involved. Re the diversion of effort: one could say the same thing about nearly every tool that has ever been developed -- the effort of creating the tool needs to be traded off against the alternative uses of this effort. Wikipedia presumably doesn't create any "new" knowledge, but makes existing knowledge accessible to a wider audience. Similarly, the discipline of putting every known mathematical proof into computer understandable form would make many of these proofs more accessible to a wider audience. This encyclopedia/database could include multiple proofs of the same theorems, as well as all kinds of human-oriented crutches -- diagrams, animations, movies, pointers to the literature, etc. In many cases, there are smart folks who may not be capable (at least not yet) of developing new theorems (they haven't imbibed enough coffee), but who are perfectly capable of translating math into computer understandable form. "Those who can, do; those who can't, translate proofs." I don't expect that such a project will uncover any significant gaps in existing proofs, but it will require significant clarifications in some cases. The overall goal of this effort would be to have mathematics put its money where its mouth is: mathematics has always claimed a higher/purer form of "truth" than other fields due to the rigor of its proofs. By building this logical structure, mathematics could "prove" this even more concretely. Ancient civilizations built pyramids, acqueducts, coliseums (colisea ?), etc., as monuments to their prowess; why can't we build such a logical structure ? At 11:42 AM 9/29/2007, Andy Latto wrote:
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