Предложение о создании компьютерной базы данных всех математических знаний
Манифест QED представлял собой предложение о создании компьютерной базы данных всех математических знаний, строго формализованной и со всеми автоматически проверяемыми доказательствами . ( QED означает quod erat demonstrandum на латыни , что означает «то, что должно быть продемонстрировано»).
Обзор
Идея проекта возникла в 1993 году, в основном под влиянием Роберта Бойера . Цели проекта, предварительно названного проектом QED или проектом QED , были изложены в манифесте QED, документе, впервые опубликованном в 1994 году при участии нескольких исследователей. [1] Явное авторство намеренно избегалось. Был создан специальный список рассылки, и состоялись две научные конференции по QED, первая в 1994 году в Аргоннских национальных лабораториях , а вторая в 1995 году в Варшаве, организованная группой Mizar . [2]
Проект, похоже, распался к 1996 году, так и не дав ничего, кроме обсуждений и планов. В статье 2007 года Фрик Видейк выделяет две причины провала проекта. [3] В порядке важности:
- Очень мало людей работают над формализацией математики. Нет убедительного приложения для полностью механизированной математики.
- Формализованная математика пока не похожа на настоящую, традиционную математику. Это отчасти связано со сложностью математической нотации, а отчасти с ограничениями существующих доказывателей теорем и помощников доказательства ; в статье делается вывод, что основные претенденты, Mizar , HOL и Coq , имеют серьезные недостатки в своих способностях выражать математику.
Тем не менее, проекты в стиле QED регулярно предлагаются. Математическая библиотека Mizar формализует большую часть математики бакалавриата и была признана крупнейшей такой библиотекой в 2007 году. [4] Похожие проекты включают базу данных доказательств Metamath и библиотеку mathlib, написанную на языке Lean . [5]
В 2014 году в рамках Венского лета логики был организован семинар «Двадцать лет Манифеста КЭД» [6] .
Смотрите также
Ссылки
- ^ Манифест QED в автоматизированной дедукции - CADE 12 , Springer-Verlag, Lecture Notes in Artificial Intelligence, том 814, стр. 238-251, 1994. HTML-версия
- ^ Отчет семинара QED II
- ^ Фрик Видейк, Новый взгляд на манифест QED, 2007 г.
- ^ Файруз Камареддин, Мануэль Маарек, Кшиштоф Ретель и Дж. Б. Уэллс, Постепенная компьютеризация/формализация математических текстов в Mizar
- ^ Библиотека mathlib https://leanprover-community.github.io/mathlib-overview.html
- ^ Двадцать лет семинару «Манифест КЭД»
Дальнейшее чтение
- Х. Барендрегт и Ф. Видейк, Проблема компьютерной математики , Труды A Королевского общества 363 № 1835, 2351–2375, 2005
- «Специальный выпуск по формальному доказательству». Извещения Американского математического общества . Декабрь 2008 г.(выпуск открытого доступа)
- Ричард А. Де Милло , Ричард Дж. Липтон , Алан Дж. Перлис , Социальные процессы и доказательства теорем и программ , Сообщения ACM , Том 22, Выпуск 5 (май 1979), Страницы: 271 - 280
- Джон Харрисон, Формализованная математика , Технический отчет 36, Центр компьютерных наук Турку (TUCS)
- Иттай Вайс, Манифест QED спустя два десятилетия Версия 2.0 , Журнал программного обеспечения, т. 11, № 8, стр. 803-815, 2016.
Внешние ссылки
- Фрик Видейк, Формализация 100 теорем Страница, отслеживающая прогресс в формализации 100 общих теорем.
- Фрик Видейк, «Семнадцать доказывающих мира», доказательство иррациональности квадратного корня из двух с помощью семнадцати различных помощников доказательства.
- «Формализованная математика» — журнал, в котором публикуются доказательства Мицара.
- Архив формальных доказательств — аналогичное (рецензируемое) хранилище доказательств в Isabelle/HOL.
- [1] Хранилище доказательств в Coq.
- UniMath «Библиотека Coq направлена на формализацию значительной части математики с использованием однозначных точек зрения»
