Up: Cooperating sites
The Mizar Group (now at the University in Bialystok - UWB) led by Andrzej Trybulec has been developing a proof checker system for almost three decades. The input language of the system, called Mizar, is close to informal mathematical language and enjoys rich linguistic structure: open vocabularies, flexible syntax, dependent types (allowing for overloading and hidden arguments), adjectives and structures (record types) with inheritance. The system is based on classical logic - Fitch-Jaskowski system of conditional proofs.
The main activities of the project are:
- evolving the language itself, and software for processing, particularly verifying the correctness of, text written in Mizar, called Mizar articles
- development of the Mizar Mathematical Library (MML) the largest repository of computer checked mathematics in the world. As of April 2003, Mizar Mathematical Library consists of 774 articles authored by ca. 130 persons from 10 countries (40 000 theorems). The articles submitted to MML, after automatic translation to English, are published in Formalized Mathematics; the electronic version is available at http://mizar.org/JFM.
UWB cooperates with KUN (Nijmegen). The cooperation includes parallel development, e.g. the formalization of a proof of FTA done almost simultaneously with some theoretical work. We continue long term and fruitful exchange of the ideas with U. of Durham (mathematical vernacular, subtyping) and other groups.
In this proposal, the group will mainly address the objective of Formal Mathematics, focussing on mathematical vernacular language and the use of ideas from type theory, such as coercive subtyping or generic metastructures (modules in Coq or locale in Isabelle), in classical mathematics.
The senior members of the Mizar Group are
- Andrzej Trybulec, contact person
- Grzegorz Bancerek
- Czeslaw Bylinski
- Adam Grabowski
- Robert Milewski
- Adam Naumowicz
- Krzysztof Retel
Bengt Nordström 2005-09-22