vdash: Future Directions	vdash Formal Math Wiki Roadmap Future
	Formalize Existing Informal Math There is a wealth of existing informal mathematics on the web: Wikipedia Mathematics Portal, PlanetMath, and MathWorld, Open access journals, preprint archives such as the ArXiv, and much else (books, journals, preprints on individual home pages, ...) Especially in the case of traditional books and journals, copyright issues may dictate that very little be copied directly into vdash. However, in many cases, the mathematical arguments themselves (as opposed to their expression in natural language) are not subject to copyright, and it may be legal to include a formal translation. In the case of the ArXiv and other LaTeX sources, the arXMLiv project may be useful for initial parsing. Statistical natural language processing techniques could, at some point, be used to make a first attempt at formalization (maybe initially put into a comment, to be moved into the actual proof over time by a human; in the worse case, an awful machine translation could merely be ignored). With appropriate tagging, this would also produce a growing body of parallel texts, to aid in subsequent translations.   Translate Existing Formal Math Large amounts of mathematics have been formalized in many systems, especially Mizar. In some cases, it may be possible to automate some of the work of translating, but even when it is not, the source documents typically are much more detailed than informal proofs, making the task much simpler. In principle, one could connect up several existing databases of formal math by merely translating the statements (and not the proofs themselves) between languages. This would preserve certainty (up to the accuracy of the translation), but is less satisfactory in terms of the explanatory power such "imported" proofs provide. There has been some work on translating proofs between the HOL systems: HOL 4, ProofPower/HOL, and HOL Light (and Isabelle/HOL via a different project). Also, in principle Isabelle/HOL documents could be mixed in with Isabelle/ZF documents. However, this would seem to be less useful than merely formalizing the statements from scratch (in idiomatic Isabelle/ZF) and then using the original proof (possibly imported as comments) as a guide to rewriting the proof in Isabelle/ZF using a declarative Isar style. Freek Wiedijk has a list of "future projects" for formal mathematics (including translations between systems, as well as specific formalizations and theoretical advances).   Improve the Formal Language Thomas Barnet-Lamb and Mohan Ganesalingam have proposed a "natural formal language" that fuses informal and formal aspects. Natural formal texts would read much like informal mathematics but with less ambiguity. Steve Kieffer, Jeremy Avigad, and Harvey Friedman have proposed an extension of ZF, augmented by definitions and partial functions. Freek Wiedijk has analyzed the proof language common to Isar and Mizar, which he calls "the mathematical vernacular".   The Theorome Project Given a substantial body of formal math in a single interlinked database, one can start to visualize the mathematical corpus in new ways. This has been done with Mizar (as a large static image, a net of structures, and a java applet of the tree of articles), though certainly there is room for more interesting visualizations, linked to live content, and with (eventually) much more mathematics. Machine learning algorithms of the sort used for clustering and topic modelling might reveal interesting structure in the usage of lemmas (for example) that cut across typical subject divisions. Aside from issues of visualizing or browsing content, Thomas Hales has likened "the formalization of just 100,000 pages of core mathematics" to "the sequencing of a mathematical genome".   Greater Automation Metis is a first-order automated theorem prover that one may run as a background process in Isabelle. As automated techniques such as SAT solvers, first-order theorem provers, SMT solvers, and projects like Larry Paulson's MetiTarski Theorem Prover advance, they can save on the number of steps of a formalized mathematical argument which need to be stated explicitly. In recent years, people have designed metasystems that use machine learning techniques to construct hybrid automated theorem provers out of diverse distinct systems, as Josef Urban's MaLARea has done. However, as John Harrison has pointed out, it is not clear how much automation we actually want. Sometimes the details are messy and uninteresting (though even in this case, we may prefer to generate details and then hide/collapse them in the display, rather than merely indicate that an external program did the work correctly). But other times, the details could be omitted (because an automated tool can instantly regenerate them), but we prefer to leave them because of their explanatory power.   Integrate Theorem Proving with Calculations Mathematical software that performs algebraic, numerical, or other sorts of calculations can sometimes be integrated with proof assistants. Some computer algebra implementations have been verified with proof assistants, and there are also methods for obtaining proofs of some calculations. Other techniques involve such tasks as generating verified code to perform a particular computer algebra task, or using existing calculation tools to obtain an oracle which a theorem prover can then use to efficiently generate a proof.   Web Widgets It is now possible to embed rendered LaTeX in ordinary documents online (via standard plugins for MediaWiki and WordPress, or via jsMath, for example). One can imagine something similar for mathematical proofs (or calculation tools, like above) — an API which enables formal arguments to be placed in the midst of webpages outside the confines of a particular site like vdash. The open mathematical software Sage already has an AJAX web interface (in individual notebooks, or via Knoboo). An interface that allowed calculations to exist outside of a notebook could usefully be embedded throughout the web, and similarly for formal proofs.   Education There are clear educational benefits to having a large body of tightly interlinked (even informal) mathematics in a common language. Formalized mathematics offers several additional benefits. One can expand or collapse proofs to show a given level of detail, but more subtle degrees of customization are also possible. Formal math could be rendered in a particularly simple "natural formal language" aimed at a specific level of mathematical maturity. The content would remain linked to the more detailed underlying proof database, and could be automatically updated as the database changes. The level of detail could dynamically scale in a fine-grained way, in response to the needs of the reader. In addition to such customizability, formal math can also be much more interactive. One could build interfaces that allow the user to experiment with, for example, changing hypotheses on theorems, as fluidly as one can control parameters on a graph via a slider today. Also, in the case of constructive existence proofs, one might input an object satisfying the hypotheses and ask for an explicit object satisfying the conclusion.   Proof Mining It is sometimes possible to use proof-theoretic techniques to extract additional constructive information from formalized results. See, e.g., Ulrich Kohlenbach's book Applied Proof Theory and papers by him and by Jeremy Avigad, Bruno Woltzenlogel Paleo, Paulo Oliva, and others.   Tools for Augmenting Human Mathematicians In 2000, Tim Gowers imagined a fascinating dialogue between a human mathematician and a computer assistant (pp. 6–11). More recently, he has imagined another conversation, the substance of which might be realized by a wiki for mathematical problem-solving techniques in the near future.   Towards a Database for Computer Mathematicians? "We are not scanning all those books to be read by people," explained one of my hosts after my talk. "We are scanning them to be read by an AI." — George Dyson, on his 2005 visit to Google (via Edge)