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:
“Those who weep for the happy periods which they encounter in history acknowledge what they want; not the alleviation but the silencing of misery.”
—Albert Camus (1913–1960)
“The reverence for the Scriptures is an element of civilization, for thus has the history of the world been preserved, and is preserved.”
—Ralph Waldo Emerson (1803–1882)
“Certainly there is not the fight recorded in Concord history, at least, if in the history of America, that will bear a moment’s comparison with this, whether for the numbers engaged in it, or for the patriotism and heroism displayed.”
—Henry David Thoreau (1817–1862)