vdash: Roadmap	vdash Formal Math Wiki Roadmap Future
	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. Besides gathering sources of new content, bots and humans can provide extensive links between vdash pages and sites such as Wikipedia and PlanetMath (in both directions), and to MathWorld. Bots could also work on the current database in the background via first-order automated tools.   Interface Improvements Parse error messages from Isabelle in a useful way. For example, a script might take subgoals noted in Isabelle error messages and expand the document with the outline: show ___ fix ___ assume ___ sorry Display attribution in a detailed manner, sorted by degree of contribution (according to various metrics). Tools for search, for expanding and collapsing parts of proofs, and for viewing the interconnections between results. and many other interface improvements...   Versioning 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: "modification of an assertion of a theorem that another theorem depends on (proofs can be modified, as long as they remain correct). modification of definition that is referenced somewhere adding an assumption to a locale ... that is referenced or removing an assumption that is referenced in a theorem proven in this locale. removing notation conventions from locales" 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.