Mizar Project

Overview

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 Resources

• 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

Mizar Services

• Mizar Forum
• Mizar User Service
• MML Query
• Mizar TWiki collaboration tool

Related Topics

• 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