Mizar System

• Overview
• Preparing a Mizar article
• Distribution
• Download

The Mizar System is the only implementation of the Mizar Language. Originally, the Mizar system was implemented on an IBM-PC x86 compatibles under MS DOS. Now we distribute releases for MS Windows, Intel-based Linux, Darwin/Mac OS X/macOS, Solaris and FreeBSD, and also Linux on PowerPC. The whole Mizar system (including verifier) is coded in Pascal using the Free Pascal compiler.

Andrzej Trybulec (1941-2013) was the author of the Mizar Language, he was also the head of the team implementing the verifier. Current Mizar implementors:

Czeslaw Bylinski (Head)

Adam Grabowski

Artur Kornilowicz

Adam Naumowicz

Karol Pąk

Josef Urban

Grzegorz Bancerek (1966-2017)

Robert Milewski

The mechanics of preparing a Mizar Article is as follows:

• The source text is prepared using any ASCII editor and typically includes from 1500 to 5000 lines.
• The text is run through the Accommodator. The directives from the Environment Declaration guide the production of the environment specific for the article. The environment is produced from the available data base.
• Now the Verifier is ready to start checking. The output contains remarks on unaccepted fragments of the source text.

When finished, an article is submitted to the Library Committee of Association of Mizar Users for inclusion into the Mizar Mathematical Library. The contributed article is subject to a review and if needed the authors must revise their file. The contents of an accepted article is extracted by the Exporter utility and incorporated into the public data base distributed to all Mizar users.

To summarize, Mizar System is based on three programs named: Accommodator, Verifier, Exporter.

The Mizar Mathematical Library is distributed under the the GPL and/or the CC-BY-SA license. The distribution of the Mizar system is freely available for download for any non commercial purposes.

NOTE: Almost all material contained in the Mizar distribution is copyrighted by the Association of Mizar Users (SUM). The source code of the Mizar verifier and accompanying tools is available to the members of SUM.

Latest official (stable) Mizar releases (version 8.1.11, MML 5.57.1412) for Win32, Linux (i386), Darwin/Mac OS X/macOS (i386)

Download via HTTP, Download via FTP

More releases

Win32 releases: HTTP, FTP

Linux (i386) releases: HTTP, FTP

Darwin/Mac OS X (i386) releases: HTTP, FTP

Solaris (i386) releases: HTTP, FTP

FreeBSD (i386) releases: HTTP, FTP

Darwin/Mac OS X (PPC) releases: HTTP, FTP

Linux (PPC) releases: HTTP, FTP

Linux (ARM) releases: HTTP, FTP