Манифест QED
Предложение о создании компьютерной базы данных всех математических знаний

Манифест 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] .

Смотрите также

Ссылки

  1. ^ Манифест QED в автоматизированной дедукции - CADE 12 , Springer-Verlag, Lecture Notes in Artificial Intelligence, том 814, стр. 238-251, 1994. HTML-версия
  2. ^ Отчет семинара QED II
  3. ^ Фрик Видейк, Новый взгляд на манифест QED, 2007 г.
  4. ^ Файруз Камареддин, Мануэль Маарек, Кшиштоф Ретель и Дж. Б. Уэллс, Постепенная компьютеризация/формализация математических текстов в Mizar
  5. ^ Библиотека mathlib https://leanprover-community.github.io/mathlib-overview.html
  6. ^ Двадцать лет семинару «Манифест КЭД»

Дальнейшее чтение

  • Х. Барендрегт и Ф. Видейк, Проблема компьютерной математики , Труды 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 направлена ​​на формализацию значительной части математики с использованием однозначных точек зрения»
Retrieved from "https://en.wikipedia.org/w/index.php?title=QED_manifesto&oldid=1184811713"