Повернутися до часової лінії

Віха · 1 січня 1989 р.

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 років за документами того часу — їх не знайдено.

Відомості про подію

Дата події
1 січня 1989 р.
Дата на часовій лінії
Дата події
Перевірка
Джерела зібрано автоматично · 27 вересня 2026 р.
Лінії
ID
evt-0885

Офіційна дата початку Mizar Mathematical Library за спогадом учасників 2005 року; першу статтю першого номера Formalized Mathematics (січень 1990 року) позначено «Received January 1, 1989». Саму мову Mizar, за тим самим спогадом, уперше представлено 14 листопада 1973 року; датованого документа того року не знайдено.

Джерела

Пов’язані події