vdash: What is vdash?	vdash Formal Math Wiki Roadmap Future
	What if Wikipedia allowed only true statements? Imagine what Wikipedia would be like, if there were a computer on the back-end that could instantly verify every submission, and allowed only true statements to be entered. Something like this is possible in mathematics, though there are many challenges to getting there.   Formal Math In principle, mathematical proofs can be written with all of the details filled in, in a way that a computer can check. Formalized mathematics and interactive theorem provers have made great progress in recent years, though in practice it can still take enormous effort to formalize results. It's time for that to change.   A Math Commons vdash is a wiki of formalized math which aims to lower the barriers to formalization. It's also one approach towards a math commons — a site with all mathematics in one place, in a common language, and in a way that anyone can edit. The main ingredients are an interactive theorem prover, a library of computer-checked mathematics, and a wiki web interface.   Why Formalize? Formalized mathematics can provide greater certainty, more detailed explanations, and instant verification. Furthermore, formal proofs can be manipulated by computers in a modular and interactive manner, and could lead to many exciting future directions in education and mathematical practice.   \vdash \vdash is the LaTeX symbol denoting logical provability.   If civilization continues to advance, in the next few thousand years the overwhelming novelty in human thought will be the dominance of mathematical understanding. — Alfred North Whitehead, "Mathematics and the good", 1941 (via The QED Manifesto)