Mathematics has undergone some rather nice developments recently with the adoption of new techologies, things like on-line journals, the arXiv, this website, etc. I imagine there must be many further developments that could be quite useful.
What I'm thinking of is a website where anyone can contribute formal proofs of theorems. In particular there would be many proofs of the same theorem provided the proof is different — like a constructive proof of Brouwer's fixed point theorem, and non-constructive proof, etc.
The idea would be to build up a large web of formal proofs, one building on another so that one could eventually do searches through this space of formal proofs to find out what the most efficient proofs are, in the sense of how many ASCII characters it would take to write-up the proof using Zermelo-Frankel set theory. One hope would be to have a big, active database of verified formal proofs. Another would be to have a webpage where you could hope to discover whether or not there are simpler proofs of theorems you know, that you may have not been be aware of.
Being a web-page there would be certain useful efficiencies — the webpage could "compile" your proof and check to see it's valid. Being a wiki would make it relatively easy for people to contribute and build on an existing infrastructure. And you'd be free to use pre-existing proofs (provided they've been verified as valid) in any subsequent proofs. One could readily check what axioms a proof needs — for example to what extent a proof needs the axiom of choice, and so on.
Is there any efforts towards such a development? Such a tool would hopefully function like the publishing arm of some sort of modern internet-era Bourbaki.
Best Answer
There are lots of sites for formal proofs, but no wiki that I am aware of.
Typical examples are:
archive of formal proofs at https://www.isa-afp.org/
Mizar http://mizar.org/
Lots of proofs are contained in the distributions of various interactive theorem provers: Isabelle, Hol, hol light, Coq, acl2 etc etc
As stated in another post, there is no agreement on foundations (formulas, axioms and rules of inference). A typical split is between classical (Hol et al.) and non-classical (Coq et al.) systems, but the differences are typically much more subtle than that. As a result all these systems are effectively unable to reuse proofs from other systems. Occasionally someone writes a translator from one system to another, but the problem here is that the translation typically does not produce a readable proof in the target system; a readable proof is necessary if the translated proof is to be maintainable. If you fix on ZFC+(maybe some other axioms), then Mizar probably has the most extensive library.
Every few years, someone proposes a big database of formal proofs, but these projects invariably die for various reasons related to the issues above. An example is the QED project:
http://en.wikipedia.org/wiki/QED_manifesto
My personal view is that constructing formal proofs, and maintaining them, is currently too difficult. Having said that, in the long run this is clearly an idea whose time will come.