Манифест КЭД

Манифест QED предлагал создать компьютерную базу данных математических знаний с автоматической проверкой доказательств.
Идея проекта возникла в 1993 году под влиянием Роберта Бойера.
Проект, названный QED project или проект КЭД, был изложен в манифесте QED, опубликованном в 1994 году.
К 1996 году проект прекратил свое существование, не добившись ничего, кроме обсуждений и планов.
В статье 2007 года Фрик Видейк выделяет две причины провала проекта: малое количество людей, работающих над формализацией математики, и отсутствие убедительного применения полностью механизированной математики.
Проекты в стиле КЭД регулярно предлагаются, включая математическую библиотеку Mizar и базу данных Metamath proof.
В 2014 году в рамках Венского лета логики был организован семинар «Двадцать лет манифесту КЭД».

Полный текст статьи:

Манифест QED