vdash: Why Use a Wiki?	vdash Formal Math Wiki Roadmap Future
	Collaboration Wikis can achieve collaboration at a scale that is difficult to reach via the traditional process of submitting completed documents to an online library. Some libraries of formalized mathematics have reached impressive size, but much more is needed if we are to eventually formalize a substantial fraction of modern mathematical knowledge.   Top-down Development Wikis also facilitate top-down development. Even if a contributor is unable to add a carefully polished layer on top of an existing curated library, he or she may be able to formalize the statement of the theorem, or give an outline (formal or informal) of the proof, for example. This contribution can be accepted by the wiki (without a checkmark indicating complete verification) and refined by others over time. Freek Wiedijk's notion of a formal proof sketch may be useful in this regard, and his articles on the formal proof sketch challenge and eight formal proof sketches provide some interesting ideas for developing this style of interaction with proof assistants further. Makarius Wenzel has written about proof sketches in Isar. In Isar, providing the word sorry as justification for a proof step causes Isabelle to move on as if the claim were actually proved. This provides a simple way to build up proof sketches within the wiki (where the final seal of approval is reserved for documents with no use of sorry in themselves or any dependencies). Eventually, vdash might interact with proof skeletons in a more elaborate way. For example, a script might take subgoals noted in Isabelle error messages and expand the document with the outline: show ___ fix ___ assume ___ sorry   Automation There are several roles for contributions by computers which might be refined by human editors over time. Some automated tools are already integrated with interactive theorem provers, e.g., the automated first-order theorem prover Metis with Isabelle. One might set up Metis to process documents in the background, occasionally filling in steps. If accepted by Isabelle, such contributions will be valid, but one will often want to rework them into more readable subproofs with explicit deductive steps. Another role might be played by bots which scrape the web for informal math, and create stubs as targets for formalization. Such bots might traverse Wikipedia Mathematics Portal, PlanetMath, and MathWorld, as well as open access journals and preprint archives such as the ArXiv. In the latter case, the arXMLiv project may be useful for initial parsing. Similarly, scripts might create new documents from existing formal libraries in other languages (with the original proof in a comment, where the licenses allow it).   Organize Mathematical Knowledge The Mathematical Knowledge Management community has many interesting ideas for organizing mathematical content, both formal and informal. In particular, some projects of MathWeb, OpenMath, OMDoc, and KWARC might eventually be integrated in various ways, to provide better search, a uniform interface for documents that allows parsing by semantic web tools, and a range of display options for mathematical notation. Similarly, tools and methods developed by organizations like Science Commons, and content from open access journals might play a larger role in the future.   Online Editing Another advantage of a web interface to proof assistants is that there is no need to install a local copy. ProofWeb provides an AJAX web interface to the Coq and Isabelle proof assistants. The interface to vdash will not be as interactive, at least initially (since partial and incomplete proofs are fine, and expected). Still, having the proof assistant on the server obviates the need for a separate local installation. Knoboo provides a similar AJAX interface to the open mathematical software Sage.   Other Wiki Approaches The MathWiki is another approach to collaboratively editing formal mathematics on the web, with somewhat different emphasis. In particular, vdash is focused on a particular language choice (Isabelle/ZF) with proofs in a human-readable declarative proof mode (Isar), with less initial emphasis on supporting multiple systems or client-side interactivity. Their proposed architecture and eventual goals are quite similar in the long run.