Mizar is a formal proof system and a mathematical language designed for the rigorous, computer-verifiable expression and checking of mathematical proofs. Developed primarily by Andrzej Trybulec and his team since the 1970s, Mizar employs a natural deduction style combined with a rich type system. Its associated repository, the Mizar Mathematical Library (MML), contains thousands of formalized theorems and definitions spanning areas such as set theory, algebra, and analysis, making it a significant resource in the formalization of mathematics.

1 History

1.1 Origins and early development (1970s–1980s)

The Mizar project began in the early 1970s at the University of Białystok (then part of Poland) under the leadership of Andrzej Trybulec, who was motivated by the vision of computer-assisted proof checking. The initial design drew on the natural deduction approach pioneered by Stanisław Jaśkowski and others, combined with a type system inspired by the AUTOMATH project of N. G. de Bruijn. The first implementation, known as "Mizar-1," was written in assembly language and ran on mainframe computers. By the late 1970s, a second version, Mizar-2, had been developed with improved parsing and type checking. Throughout the 1980s, the system was refined, and a formal language specification was published, leading to the stable Mizar-3 release. The earliest formalizations were concentrated on elementary set theory and algebraic structures.

1.2 Key milestones and releases

In the 1990s, the Mizar team released Mizar-4, which introduced a more modular article structure and the concept of "registrations" for automatic type expansion. The year 2000 saw the first release of Mizar-7, which became the standard for many years and was accompanied by the rapid growth of the Mizar Mathematical Library (MML). Subsequent milestones include the introduction of a new syntax for reserved words (2005), the addition of "theorems with conditions" (2009), and the transition to a Unicode-based proof checker in the 2010s. The current mainline version, Mizar-8, has been in continuous development since the late 2000s.

1.3 Mizar version history

The version numbering follows the pattern Mizar-X, where X is an integer. Mizar-1 through Mizar-3 are considered early prototypes. Mizar-4 and Mizar-5 (1990s) established the core language. Mizar-6 (late 1990s) introduced the checker as a separate tool. Mizar-7 (2000–2008) was a long-lived stable series. Mizar-8 (2009–present) brought a rewritten kernel, improved error messages, and support for modern operating systems. Each major version retains backward compatibility for the MML, though occasional deprecations occur.

2 Language and Syntax

2.1 Grammar and lexical structure

The Mizar language is a context-free grammar with keywords written in all capitals (e.g., theorem, definition, let). Comments are enclosed in :: and extend to the end of the line. Terms and formulas are built from identifiers (starting with a letter, then alphanumeric or underscore), numeric literals, and punctuation. Parentheses and brackets are used for grouping. The grammar distinguishes between "vocative" expressions (for type attributions) and "formula" expressions (for logical propositions). Line breaks and indentation are insignificant; semicolons separate statements.

2.2 Reserved words and symbols

Mizar uses a fixed set of about 200 reserved words, including theorem, proof, assume, thus, then, hence, let, be, such that, definition, registration, scheme, func, pred, mode, and many others. Punctuation symbols include :, ::, ;, ., ,, ( ), [ ], and the logical connectives & (and), or (or), => (implies), <=> (iff), not (negation). Equality is denoted by =. Variable binding uses -> for lambda-like constructs in type definitions.

2.3 Types and term construction

The type system of Mizar is based on a hierarchy of "modes" (sortal types) and "attributes" (properties). Every term has a type, declared with be (e.g., let x be Nat). Types can be structured: set is the universal type; Nat is the type of natural numbers; Elem of D denotes an element of a set D. Functions are defined as func f(arg1 being T1, ...) -> T2. Predicates are pred P(arg1 being T1, ...). Types can be parametrized by terms, enabling dependent types in a limited fashion. Terms are constructed by constants, variables, function applications, and set-formers.

2.4 Statements: theorems, definitions, and registrations

The fundamental statements in Mizar are:

  • Theorems: theorem T: P where P is a formula. A proof follows after the keyword proof ... end;.
  • Definitions: definition blocks can introduce functions (func), predicates (pred), modes (mode), attributes (attr), and structures (struct). Each definition requires a correctness justification (e.g., existence of a set for a mode).
  • Registrations: registration blocks allow the user to assert new properties of types (e.g., cluster registrations that say "non empty set is non empty", or "let a,b be Nat; cluster a+b -> Nat"). Registrations are used to automatically infer type information and reduce the proof burden.

3 Proof Checking

3.1 Verification algorithms and inference rules

Mizar's proof checker implements a natural deduction calculus with a small kernel of inference rules, including modus ponens, universal generalization, existential instantiation, and rules for equality. The checker converts a proof text into an internal representation and verifies each step against the current context (known theorems, definitions, registrations). The underlying logic is that of the Tarski–Grothendieck set theory (a variant of ZFC with universes). The rules are designed to be sound and complete with respect to this set theory. A key component is the "deduction theorem" handling: from an assumption A, the proof must derive B to conclude A => B.

3.2 Error handling and diagnostic messages

When a proof step is invalid, the Mizar checker issues an error message that indicates the line number, the nature of the error (e.g., "This inference is not accepted", "Type mismatch"), and often a hint about which rule could be applied. Errors are grouped by severity: syntax errors, environment errors (missing definitions), and logical errors. The checker also issues warnings for redundant steps or inefficient code. The error messages are designed to be read by humans and have been improved over versions to include suggested corrections.

3.3 Performance and scalability

Proof checking in Mizar is generally fast because the kernel is small and the proof language is explicit. For a typical article of a few hundred lines, checking takes less than a second on modern hardware. For larger articles (thousands of lines), checking remains under a minute. The MML, containing over 50,000 theorems, can be checked in batch in a few hours. The system scales to large proofs because registrations allow automatic type inference, reducing the need for explicit steps. Memory usage is also moderate. However, very deep proof trees or a large number of dependencies can slow down checking.

4 Mizar Mathematical Library (MML)

4.1 Structure and organization (articles, dependencies)

The MML is a collection of &quot;articles&quot; (text files with .mizar extension), each containing a set of definitions, theorems, and proofs. Articles are organized hierarchically by topic (e.g., SETFAM_1 for set families, REAL_1 for real numbers). Dependencies are declared at the top of each article using the vocabularies, requirements, notations, constructors, and theorems directives. The library is designed to be acyclic: each article can use only those resources that are already defined in articles it explicitly cites. The structure ensures that the entire library can be checked in a consistent order.

4.2 Notable formalizations (e.g., JFM, CANTOR, REALS)

Several major formalizations reside in the MML:

  • JFM (Journal of Formalized Mathematics): A subset of the library that was published in a dedicated journal. It includes foundational material like set theory and basic algebraic structures.
  • CANTOR: A series of articles on cardinal and ordinal arithmetic, including the formalization of Cantor's theorem and the Schröder–Bernstein theorem.
  • REALS: Articles formalizing the real numbers as Dedekind cuts, including completeness, limits, and elementary analysis.
  • TOPOLOGY: A substantial collection on general topology, including separation axioms and compactness.
  • GRAPH: Formalizations of graph theory, including planar graphs and Kuratowski's theorem.

4.3 MML versioning and maintenance

The MML is versioned in lockstep with the Mizar checker releases. Each major version (e.g., MML 5.0, MML 6.0) corresponds to a specific release of the checker. Revisions are tracked via a Git repository, and the library undergoes periodic &quot;corrections&quot; where outdated theorems are replaced and new formalizations are added. The maintainers (from the Mizar project team and volunteers) ensure backward compatibility: existing articles continue to pass after an MML update, unless a definition has been fundamentally changed.

4.4 Tools for navigating the library (MMLQuery, MizarWiki)

Two main tools facilitate navigation:

  • MMLQuery: A web-based search engine that allows users to query the MML by symbol, theorem name, or textual pattern. It returns the full text of definitions and theorems, plus dependency information.
  • MizarWiki: A community-maintained wiki that provides articles, tutorials, and documentation for the MML. It includes cross-references, usage examples, and discussion pages.

Additionally, the Mizar distribution includes a command-line tool mizf (find) for local searches.

5.1 Mizar Mode (Emacs, Visual Studio Code)

To facilitate proof authoring, the Mizar project provides &quot;Mizar Mode&quot; plugins for popular editors.

  • Emacs Mizar Mode: Offers syntax highlighting, indentation, and integration with the Mizar checker. It includes shortcuts for running the checker, navigating errors, and inserting common proof templates.
  • Visual Studio Code Mizar Extension: A more recent addition, providing similar features with an LSP (Language Server Protocol) backend. It supports auto-completion, hover definitions, and inline error reporting.

5.2 Web interfaces (MMLQuery, Mizar on Jupyter)

Beyond MMLQuery, the system is accessible via web:

  • Mizar on Jupyter: A Jupyter notebook kernel that allows interactive proof development in a browser. Users can write Mizar code in cells and run the checker, viewing the output inline.
  • TryMizar: An online sandbox (available at try.mizar.org) where visitors can experiment with proof snippets without installing the system.

5.3 Comparison with other proof assistants (Coq, Isabelle, Lean)

Mizar differs from other major proof assistants in several respects:

  • Coq: Uses dependent type theory and is more expressive for complex inductive types, but has a steeper learning curve. Mizar's natural deduction style is closer to traditional mathematical writing.
  • Isabelle: Is a generic proof assistant with multiple object logics (most notably Isabelle/HOL). Both Mizar and Isabelle emphasize readability of proofs, but Isabelle's "apply-style" scripts can be less explicit than Mizar's declarative style.
  • Lean: A younger system (launched 2013) that combines a powerful type theory with a large library (mathlib). Lean has a more expressive tactic language but lacks the long-term backward compatibility of MML. Mizar remains distinct in its adherence to a single set-theoretic foundation and its huge library of fully explicit proofs.

6 Community and Usage

6.1 Annual conferences (Mizar Workshops)

The Mizar project organizes an annual event called the &quot;Mizar Workshop&quot; (often co-located with the Conference on Intelligent Computer Mathematics, CICM). The workshops bring together developers, users, and students to present new formalizations, discuss system improvements, and plan the library&#039;s evolution. The proceedings are published in the Formalized Mathematics journal series.

6.2 Educational applications (mathematics courses, teaching logic)

Mizar has been used in university courses in Poland and elsewhere to teach mathematical logic and formal reasoning. The system's clear separation of declaration and proof, along with detailed error messages, makes it suitable for undergraduate courses. Several textbooks and online tutorials (e.g., "Mizar in a Nutshell") exist. The system helps students understand the structure of proofs and the need for precision.

6.3 Impact on automated theorem proving and formal verification

The Mizar library has been a source of mathematical knowledge for automated theorem provers (ATPs). The &quot;MPTP&quot; (Mizar Problems for Theorem Proving) project extracts problems from the MML in TPTP format, used to benchmark ATP systems. Mizar proofs have also been used to generate training data for machine learning in theorem proving. In formal verification, the Mizar approach of explicit human-authored proofs contrasts with automated verification, but its library serves as a trusted repository. The system has influenced the design of later proof languages, such as ForTheL and Naproche.