Mizar

The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec. Wikipedia

Created Year: 1973
Designed by: Andrzej Trybulec
Aliases: Mizar system

Wikidata: Q1609529

Programming paradigms: declarative programming