History
The Mizar Project was started around 1973 by Andrzej Trybulec as an attempt to reconstruct mathematical vernacular so it can be checked by a computer. Its current goal, apart from the continual development of the Mizar System, is the collaborative creation of a large library of formally verified proofs, covering most of the core of modern mathematics. This is in-line with the influential QED manifesto.
Currently the project is developed and maintained by research groups at Białystok University, Poland, the University of Alberta, Canada, and Shinshu University, Japan. While the Mizar proof checker remains proprietary, the Mizar Mathematical Library – the sizable body of formalized mathematics that it verified – is licensed open-source.
Papers related to the Mizar system regularly appear in the peer-reviewed journals of the mathematic formalization academic community. These include Studies in Logic, Grammar and Rhetoric, Intelligent Computer Mathematics, Interactive Theorem Proving, Journal of Automated Reasoning and the Journal of Formalized Reasoning.
Read more about this topic: Mizar System
Famous quotes containing the word history:
“History does nothing; it does not possess immense riches, it does not fight battles. It is men, real, living, who do all this.... It is not “history” which uses men as a means of achieving—as if it were an individual person—its own ends. History is nothing but the activity of men in pursuit of their ends.”
—Karl Marx (1818–1883)
“The History of the world is not the theatre of happiness. Periods of happiness are blank pages in it, for they are periods of harmony—periods when the antithesis is in abeyance.”
—Georg Wilhelm Friedrich Hegel (1770–1831)
“The history of medicine is the history of the unusual.”
—Robert M. Fresco, and Jack Arnold. Prof. Gerald Deemer (Leo G. Carroll)