Vdash is a new proposal for a formalized mathematics Wiki, by Cameron Freer . The slides on the Vdash site present a screenshot with an Isabelle/HOL proof, but from the mailing list one can find out that the Wiki is going to be based on Isabelle/ZF. The slides mention a possibility of importing formalized proofs from IsarMathLib as part of the initial library. Cameron’s ideas are perfectly aligned with what I think such Wiki should look like. Needless to say I will be a happy contributor when Vdash becomes a reality.