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