Metamath and the art of mathematics

My brilliant coworker G.D. thinks Metamath, and the successor I envision (in the previous entry), are sort of pointless.

I think his main beef with the idea is this: people prove things by inventing crazy new concepts that won't get formalized for a long time. This inventiveness is the really interesting part of math. I think G.D.'s impression is that just about any proof you read in a mathematical journal today probably can't be put into a formal, machine-checkable form for decades to come.

He is probably right. So my hypothetical checked theorem database can never be up-to-the-minute. Then what value could it have?

• Exploration and education. Even if the database only covers formally grounded math, I think that could get us up to maybe 1950. Number theory is pretty well grounded, I think. Real analysis. Calculus. Euclidean geometry. Group theory. Think how huge it would be. Thousands of human-readable proofs, every step checked, and you can drill down into any step if you don't understand the reasoning. Basically every theorem an undergrad ever bumps into; every theorem I personally could ever hope to understand. It sounds exciting to me.

• Finding assumptions. Does the fundamental theorem of calculus depend on the axiom of choice? Metamath doesn't have that theorem yet, but when it does, then you'll know. Exposing previously hidden assumptions sounds good for math.

• Finding gaps. Check out the axiom of choice. Here's a discovery that rocked mathematics. Are there any more of these still lurking in standard math? It seems wildly unlikely... but then, it also seems unlikely that what we've got is that perfect.

• Mathematician productivity. The ultimate (200-year) goal is to evolve the system into a work environment for mathematicians. If you started every expedition by plunking your conjecture into a worksheet, every once in a while the program could immediately respond with the (known or easily found) proof. Also, Andrew Wiles's first proof of Fermat's last theorem was found to contain a serious error that it took him a year to fix. Of course he would have preferred to have discovered that prior to publication. The current proof is 200 pages; I doubt it's been scrutinized. These thoughts make this idea seem inevitable. It just sounds too useful as a dumb tool.

And: I think the time gap between a new invention in math and its formal grounding has been shrinking. Maybe formalism will catch up to discovery!

I think the essential question is this: do you think the Zermelo-Fraenkel axioms really are one of humankind's most profound achievements? Or were these guys just mincing grammar snobs, coming in after the Newtons and Galoises of the world, acting all important, dotting the i's and crossing the t's—only to get blown out of the water by Gödel before they even finished the job?