|vdash: What is vdash?|
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.
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.
\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.