Has anyone thought about creating a formal proof wiki with verifier?

There are lots of sites for formal proofs, but no wiki that I am aware of.

Typical examples are:

archive of formal proofs at https://www.isa-afp.org/

Mizar http://mizar.org/

Lots of proofs are contained in the distributions of various interactive theorem provers: Isabelle, Hol, hol light, Coq, acl2 etc etc

As stated in another post, there is no agreement on foundations (formulas, axioms and rules of inference). A typical split is between classical (Hol et al.) and non-classical (Coq et al.) systems, but the differences are typically much more subtle than that. As a result all these systems are effectively unable to reuse proofs from other systems. Occasionally someone writes a translator from one system to another, but the problem here is that the translation typically does not produce a readable proof in the target system; a readable proof is necessary if the translated proof is to be maintainable. If you fix on ZFC+(maybe some other axioms), then Mizar probably has the most extensive library.

Every few years, someone proposes a big database of formal proofs, but these projects invariably die for various reasons related to the issues above. An example is the QED project:

http://en.wikipedia.org/wiki/QED_manifesto

My personal view is that constructing formal proofs, and maintaining them, is currently too difficult. Having said that, in the long run this is clearly an idea whose time will come.

Such a thing does exist; check out http://www.vdash.org/ and also this talk by Cameron Freer: http://www.youtube.com/watch?v=ZDI7L4Ya9Ms.

I think the following additional links are relevant:

http://homepages.inf.ed.ac.uk/da/mathwiki/

http://prover.cs.ru.nl/wiki.php

http://www.qedeq.org/ (sort of)

However, like David Lehavi I'm skeptical about the benefit of wikis over regular proof assistant technology. For me, the entrance barrier has always been learning the language and tactics of a proof assistant, not installing the software or adding something to the standard library (that is, I have never gotten that far, but if it's a problem, then it's a social one).

I agree with Tom Ridge that the time for a big collection of formal mathematics will come. But I think we should collect definitions, theorem statements, and proofs separately. That is, if a theorem is already widely known to be true, the proof should be optional, so it can be filled in later. A collection of formalized definitions and known facts would already be very useful, and most importantly, people working on different proofs can collaborate easily, whereas the formalization of definitions and theorem statements requires coordination. Of course, with current proof assistants, it's hard to be certain that definitions and statements are correct ...