Loading article…
QEDマニフェストは、厳密に形式化され、すべての証明が自動的に検証された、あらゆる数学的知識を網羅したコンピュータベースのデータベースの提案であった。（QEDはラテン語でquod erat demonstrandum、つまり「証明されるべきもの」を意味する。）
このプロジェクトのアイデアは、主にロバート・ボイヤーの働きかけにより、1993 年に生まれました。暫定的にQED プロジェクトまたはプロジェクト QEDと名付けられたこのプロジェクトの目標は、複数の研究者の意見を取り入れて 1994 年に初めて公開された文書である QED マニフェストに概説されています。[ 1 ]明示的な著者は意図的に避けられました。専用のメーリングリストが作成され、QED に関する 2 つの科学会議が開催されました。最初の会議は 1994 年にアルゴンヌ国立研究所で、2 回目は 1995 年にワルシャワでミザールグループによって組織されました。[ 2 ]
このプロジェクトは1996年までに解散したようで、議論や計画以上の成果は何も生み出さなかった。2007年の論文で、フリーク・ヴィーディックはこのプロジェクトの失敗の理由を2つ挙げている。[ 3 ]重要度順に：
それにもかかわらず、QED スタイルのプロジェクトは定期的に提案されている。Mizar数学ライブラリは、学部レベルの数学の大部分を形式化しており、2007 年時点ではそのようなライブラリとしては最大規模であった。[ 4 ] 同様のプロジェクトには、Metamath証明データベースやLeanで書かれた mathlib ライブラリなどがある。[ 5 ]
2014年には、ウィーン・サマー・オブ・ロジックの一環として、QEDマニフェスト[ 6 ]の20周年ワークショップが開催されました。