Monotone + ikiwiki + IsarMathLib + Isabelle|
The initial version of vdash (coming soon) will consist of a distributed revision control system (most likely Monotone or Git), a wiki interface (ikiwiki), initially seeded by content (IsarMathLib), with a simple script by which the proof assistant (Isabelle) approves valid new contributions.
Build Content and Community
This is, of course, much more easily said than done. However, it should be possible to seriously develop the wiki even with just the above, before subsequent improvements to the infrastructure and interface.
In addition to encouraging systematic extensions of IsarMathLib and free-form proof outlines of larger results (which can later be edited so as to have a more uniform style and notation), it may be useful to organize challenge problems, to motivate the community and build up content in particular directions.
Isabelle Verification Server(s)
Eventually an instance of Isabelle might interact with the revision control repository via a simple queue interface, and could be on a different server. There are various proposals for how Isabelle might asynchronously process proof documents, by Makarius Wenzel, Holger Gast, and Nikos Drakos and Ross Moore.
Though this is not an initial priority, it opens the possibility of cloneable images of the verifiers (by far the most computationally intensive part) for use on EC2 or for anyone who wants to contribute server time. There are of course serious issues of integrity and trust, but one can imagine an eventual ecosystem of verifiers which sign their certificates of validity, along with a network of trust similar to public-key servers.
Connect to Other Math
Bots could crawl existing sources of informal math and create automated feeds/scrapes from open-access sources (with appropriate licenses) that turn into stubs as targets for formalization.
Bots could also work on the current database in the background via first-order automated tools.
A method of locking-down verified pages should help greatly in preventing abuse of completed documents. Perhaps one could allow arbitrary edits of unverified pages, but only edits of verified pages that are themselves correct (or allow only forks).
One would also like a mechanism whereby only certain changes to documents (on which others depend) automatically update the references. In the meantime, Slawomir Kolodynski has proposed that banning the following operations may suffice:
Eventually, with more sophisticated versioning, one might allow any revision, but not automatically update references to it, unless it didn't do any of the above.
Slides 14–39 of a MathWiki proposal outline several more complicated possibilities involving both links that automatically point to the new statement, as well as static links to the old version.