Mizar: бібліотека перевіреної математики
1 січня 1989 року до бази даних проєкту Mizar Анджея Трибульця в Білостоці внесли перші три статті, і цю дату учасники називають офіційним початком Mizar Mathematical Library — зібрання математичних текстів, кожен рядок яких перевіряє машина. До кінця 1989 року статей було 66; з січня 1990 року вони виходили друком у журналі Formalized Mathematics.
Чому це важливо
Перевірка доведень машиною перестала бути перевіркою окремих текстів і стала спільною бібліотекою, до якої різні автори додають статті, що спираються одна на одну. Це редакційна оцінка.
Перша стаття першого номера Formalized Mathematics — «Tarski Grothendieck Set Theory» Трибульця (Варшавський університет, Білосток), «перша частина аксіоматики системи Mizar», позначена «Received January 1, 1989». Попередню історію знаємо лише зі спогаду учасників 2005 року: назва з'явилася наприкінці 1972 року, Трибулець уперше представив ідею 14 листопада 1973 року на семінарі у Варшавському університеті, перші експерименти відбулися восени 1974 року на польській машині ODRA-1204, а версію Mizar-PC для числення висловлень із натуральним виведенням у стилі Яськовського 1975–1976 років використовували в навчанні. Проєкт починався в Плоцькому науковому товаристві, з 1976 року — у Білостоці. 2005 року бібліотека мала 855 статей. Чого запис не стверджує: що Lean чи інші пізніші системи походять від Mizar — прочитані джерела цього не кажуть; дат 1973–1975 років за документами того часу — їх не знайдено.