From Wikiproofs
Jump to: navigation, search
Back to main page About Wikiproofs
A short outline of Wikiproofs.

Wikiproofs is a repository of automatically verified proofs. The project is collaborative in nature, meaning that anyone can add new content or improve existing proofs. The content of Wikiproofs is also free in the sense that anyone can distribute or modify the textual contents of Wikiproofs under the terms of the Creative Commons Attribution-Share Alike 3.0 Unported Licence.

The goal of Wikiproofs is to collect both formal and informal proofs of all important theorems of mathematics, formal logic and possibly other formalisable systems. For this purpose, Wikiproofs is backed by JHilbert, a very simple and flexible proof verifier.

Hilbert's program[edit]

It was the idea of mathematician David Hilbert to formalise as much as possible of the body of extant mathematics. In fact, he proposed to formalise all existing theories based on a set of universal axioms and then prove soundness and completeness. This was later proved to be impossible by Kurt Gödel. Nevertheless, Wikiproofs strives to implement those parts of Hilbert's program which are possible and interesting.

The JHilbert proof verifier[edit]

For the formalisation of all mathematics to be possible, a simple and flexible proof verifier is required. Most proof verifiers and automated theorem provers have a very specific complex metalogic already built in. JHilbert, in contrast, uses only a few very simple concepts (simple substitution rule, disjoint variable constraints, stack-based proofs). This makes it at least in some way adaptable to virtually all mathematics.

These very simple but highly effective concepts go back to the work of Norman Megill, who implemented them in his Metamath program. On his highly recommended metamath website, thousands of proofs can be browsed at leisure.

Later, Raph Levien developed the Metamath concepts into Ghilbert, enriching them (among other things) with definitions and module support.

JHilbert is the continuation of Ghilbert. It started out as a clone and is still largely identical with Ghilbert.

Without David Hilbert, Norman Megill and Raph Levien, the Wikiproofs project would not have been possible.

Proofs live in wiki pages[edit]

Putting proofs in wiki pages is not just a convenient way of getting proofs up on the web. A wiki is built for collaboration, and getting a sufficient body of collaborators is key to the success of any formalized math project.

Another key goal of the wiki is that we want to be able to intersperse formal proofs with text (formatted using italics, headers, etc), images (for example, diagrams in geometry proofs), formulas (in TeX or unicode text), and anything else that can be done by mediawiki (the wiki which we use, which is also used for wikipedia and many other wikis).