Mizar is a system used to represent mathematical vernacular so that it can be read and manipulated by humans and verified by computers. The Mizar Project began in 1973 and continues at the University of Bialystok in Poland. The computer formalization of mathematics is a daunting task; currently, the project has created a database with over 2,000 definitions of mathematical concepts and more than 30,000 theorems. The project's Web site has a complete description of the Mizar language syntax and offers free downloads of the Mizar system and mathematical library for non-commercial use. In the Journal of Formalized Mathematics section, there is information about submitting articles to contribute to the project. This site is mainly geared toward researchers and mathematicians.