PlanetMath is a virtual community which aims to help make mathematical knowledge more accessible. PlanetMath's content is created collaboratively: the main feature is the mathematics encyclopedia with entries written and reviewed by members. The entries are contributed under the terms of the Creative Commons By/Share-Alike License in order to preserve the rights of authors, readers and other content creators in a sensible way.
PlanetMath entries are written in LaTeX, the lingua franca of the worldwide mathematics community. All of the entries are automatically cross-referenced with each other, and the entire corpus is kept updated in real-time.
The Mizar project started around 1973 as an attempt to reconstruct mathematical vernacular in a computer-oriented environment.
Since 1989, the most important activity in the Mizar project, apart from continual improvement of the Mizar System, has been the development of a database for mathematics. International cooperation (the main partners: Shinshu University in Nagano and University of Alberta in Edmonton) resulted in creating a database which includes more than 7000 definitions of mathematical concepts and more than 40000 theorems (see Merak MML Browsing for more statistics).