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).
N. Oldager. Proceedings of the 11th International Conference on Conceptual Structures (ICCS 2003), volume 2746 of Lecture Notes in Computer Science, page 69-82. Springer, (2003)