Mizar: a library of checked mathematics
On 1 January 1989 the first three articles were entered into the database of Andrzej Trybulec's Mizar project in Białystok, and the participants call this the official start of the Mizar Mathematical Library, a collection of mathematical texts every line of which a machine checks. By the end of 1989 there were 66 articles; from January 1990 they were printed in the journal Formalized Mathematics.
Why it matters
Machine checking of proofs stopped being the checking of single texts and became a shared library, to which different authors add articles that rest on one another. This is an editorial assessment.
The first article of the first issue of Formalized Mathematics is Trybulec's 'Tarski Grothendieck Set Theory' (Warsaw University, Białystok), 'the first part of the axiomatics of the Mizar system', marked 'Received January 1, 1989'. The earlier history is known only from the participants' account of 2005: the name appeared in late 1972, Trybulec first presented the idea on 14 November 1973 at a seminar at Warsaw University, the first experiments took place in the fall of 1974 on the Polish ODRA-1204, and Mizar-PC, for propositional calculus with natural deduction in Jaśkowski's style, was used in teaching in 1975-1976. The project began at the Płock Scientific Society and has been in Białystok since 1976. In 2005 the library held 855 articles. What the record does not claim: that Lean or other later systems descend from Mizar, which the sources read do not say; the dates of 1973-1975 from documents of that time, which were not found.