Кіріспе
Барлық математикалық білімнің компьютерлік базасын құру туралы ұсыныс. 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 жобасы немесе QED жобасы деп аталған жобаның мақсаттары 1994 жылы бірнеше зерттеушілердің қатысуымен алғаш рет жарияланған QED манифестінде баяндалған. Авторлық құқығын көрсетуден мұқият бас тартылды. Арнайы электрондық пошта тізімі құрылды және QED тақырыбында екі ғылыми конференция өтті, біріншісі 1994 жылы Аргонн Ұлттық зертханасында, екіншісі 1995 жылы Варшавада Mizar тобы ұйымдастырды. Жоба 1996 жылға қарай тоқтатылған сияқты, нәтижесінде талқылаулар мен жоспарлардан басқа ештеңе тумады. 2007 жылғы мақалада Фрик Видейк жобаның сәтсіздігіне екі себепті анықтады. Маңыздылығы бойынша:
Математиканы формалдаумен айналысатын адамдар өте аз. Толық автоматтандырылған математикаға нақты қажеттілік жоқ. Формалдау арқылы алынған математика әлі де нақты, дәстүрлі математикадан өзгеше. Бұл математикалық нотацияның күрделілігіне және қазіргі теореманы дәлелдейтін жүйелердің шектеулеріне байланысты; мақалада негізгі талапкерлер – Mizar, HOL және Coq математиканы бейнелеу мүмкіндіктерінде елеулі кемшіліктері бар екені көрсетілді. Дегенмен, QED стиліндегі жобалар үнемі ұсынылып тұрады. Mizar математикалық кітапханасы бакалавриат деңгейіндегі математиканың үлкен бөлігін формалдайды және 2007 жылы осындай ең ірі кітапхана деп есептелді. Осыған ұқсас жобаларға Metamath дәлелдеулер базасы және Lean тілінде жазылған mathlib кітапханасы жатады. 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.