Введение
Предложение о создании компьютерной базы данных всех математических знаний. Манифест QED представлял собой предложение создать компьютерную базу данных всех математических знаний, строго формализованную, с автоматической проверкой всех доказательств. (Q. E. D. – латинское сокращение от quod erat demonstrandum, означающее «что и требовалось доказать»).
The QED manifesto was a proposal for a computer based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically. (Q. E. D. means quod erat demonstrandum in Latin, meaning "which was to be demonstrated.")
Обзор
Идея проекта возникла в 1993 году, главным образом благодаря усилиям Роберта Бойера. Цели проекта, предварительно названного QED project или project QED, были изложены в манифесте QED – документе, впервые опубликованном в 1994 году при участии нескольких исследователей. Явное авторство было намеренно не указано. Был создан специальный список рассылки, и состоялись две научные конференции по QED: первая в 1994 году в Национальных лабораториях Аргонн, а вторая в 1995 году в Варшаве, организованная группой Mizar. Проект, по всей видимости, прекратил своё существование к 1996 году, не приведя ни к каким результатам, кроме обсуждений и планов. В статье 2007 года Фрик Видейк выделяет две основные причины провала проекта. В порядке значимости: очень небольшое количество людей занимается формализацией математики; отсутствует убедительное практическое применение полностью механизированной математики; формализованная математика пока не соответствует реальной, традиционной математике. Это обусловлено, с одной стороны, сложностью математической нотации, а с другой – ограничениями существующих систем доказательства теорем и ассистентов доказательства; в статье отмечается, что ведущие системы, такие как Mizar, HOL и Coq, имеют серьёзные недостатки в выражении математических концепций. Тем не менее, проекты в стиле QED регулярно предлагаются. Математическая библиотека Mizar формализует значительную часть математических дисциплин бакалавриата и в 2007 году считалась крупнейшей библиотекой такого рода. К аналогичным проектам относятся база данных доказательств Metamath и библиотека mathlib, написанная на языке Lean. В 2014 году в рамках Венской летней школы логики был организован семинар, посвящённый двадцатилетию манифеста QED.
Very few people are working on formalization of mathematics. There is no compelling application for fully mechanized mathematics. Formalized mathematics does not yet resemble real, traditional mathematics. This is partly due to the complexity of mathematical notation, and partly to the limitations of existing theorem provers and proof assistants; the paper finds that the major contenders, Mizar, HOL, and Coq, have serious shortcomings in their abilities to express mathematics. Nonetheless, QED style projects are regularly proposed. The Mizar Mathematical Library formalizes a large portion of undergraduate mathematics, and was considered the largest such library in 2007. Similar projects include the Metamath proof database and the mathlib library written in Lean. In 2014 the Twenty years of the QED Manifesto workshop was organized as part of the Vienna Summer of Logic.