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. In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.

Property Value
dbo:abstract
  • 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. In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence. (en)
dbo:designer
dbo:influenced
dbo:influencedBy
dbo:thumbnail
dbo:wikiPageEditLink
dbo:wikiPageExternalLink
dbo:wikiPageExtracted
  • 2019-06-14 02:29:14Z (xsd:date)
dbo:wikiPageHistoryLink
dbo:wikiPageID
  • 209074 (xsd:integer)
dbo:wikiPageLength
  • 12184 (xsd:integer)
dbo:wikiPageModified
  • 2019-06-08 16:04:07Z (xsd:date)
dbo:wikiPageOutDegree
  • 54 (xsd:integer)
dbo:wikiPageRevisionID
  • 900937922 (xsd:integer)
dbo:wikiPageRevisionLink
dbp:wikiPageUsesTemplate
dct:subject
rdf:type
rdfs:comment
  • 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. In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence. (en)
rdfs:label
  • Mizar system (en)
owl:sameAs
foaf:depiction
foaf:homepage
foaf:isPrimaryTopicOf
foaf:name
  • Mizar (en)
  • (en)
foaf:page
is dbo:knownFor of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is foaf:primaryTopic of