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 9400 definitions of mathematical concepts and more than 49000 theorems (see Megrez MML Browsing for more statistics).

- Mizar Language
- Mizar System
- Bibliography of Mizar Project
- Formalized Mathematics
- Mizar Project at the University of Alberta
- Mizar Project at Shinshu University
- Freek Wiedijk's Page about Mizar
- Josef Urban's Mizar Mode for Emacs

- MKM Interest Group
- The QED Project and QED related material
- MathML
- MathWeb - Supporting mathematics on the Web
- OMDoc - Open Mathematical Documents
- The CALCULEMUS Project
- The TYPES Project
- Mechanized Reasoning
- Formal Methods
- The HELM Project
- HOL Mechanical Theorem Proving System
- Journal of Automated Reasoning (JAR)
- Formalized Mathematics (DRAFT) by John Harrison
- The New York Times article on the automatic proof of Robbins's conjecture
- Automath Archive

[ Home | Project | Language | System | People | MML | FM | SUM ]

Last modified: May 17, 2010