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:
“Both place and time were changed, and I dwelt nearer to those parts of the universe and to those eras in history which had most attracted me.”
—Henry David Thoreau (1817–1862)
“False history gets made all day, any day,
the truth of the new is never on the news
False history gets written every day
...
the lesbian archaeologist watches herself
sifting her own life out from the shards she’s piecing,
asking the clay all questions but her own.”
—Adrienne Rich (b. 1929)
“The history of all countries shows that the working class exclusively by its own effort is able to develop only trade-union consciousness.”
—Vladimir Ilyich Lenin (1870–1924)