On 9/29/07, Henry Baker <hbaker1@pipeline.com> wrote:
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.
Maybe my experience is too many years out of date, but I find computer-understandable proofs to make them much less accessible in general. For instance, in geometry you need to use something closer to Hilbert's approach, and spend (waste?) lots of time on proving that this point is between those two, or this ray is between those two, so you can add or subtract distances or angles. Of course, it's essential to prove those things to make proofs rigorous, but rigor and accessibility are quite different things, and I think negatively correlated.
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.
Creating a database of proofs with links, like a wiki, makes a lot of sense to me. Writing the proofs in a form where they can be verified by a computer does not.
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."
Sure, as a part of a full employment act for semicompetent amateur mathematicians, it might be OK. But I'd rather see them, say, working on some housekeeping tasks on OEIS.
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.
Along these lines, has anyone read the new novel _A Certain Ambiguity_? I met the author recently and have almost finished the book. It's a pretty good read and certainly quite focused on exactly this question: is mathematics a higher form of truth?
Ancient civilizations built pyramids, acqueducts, coliseums (colisea ?), etc., as monuments to their prowess; why can't we build such a logical structure ?
Again, the idea of a database of proofs with links to diagrams, alternate proofs, explanations, and so on, sounds great. Working with automated proof checking sounds painful. --Joshua Zucker