QEDマニフェスト／QEDプロジェクト
"Preface: Twenty Years of the QED Manifes" というPDF文書がある。これはアクセスするとダウンロードされてしまう2ページの文書。ここで要約しておく。
QEDマニフェストとワークショップが1994,5,6あたりに行われたので、2014,5,6あたりで20周年になる。当該文書は2016年に書かれたもの。
QEDプロジェクトは、マシンチェッカブルな形で数学資産を構築するプロジェクト。数学資産とは、数学的な知識とノウハウ（テクニック）の集まり。こういう試みと努力は QED-style efforts と呼ぶ。
QEDスタイルエフォートの実例はMizarのMMLだろう。他に、seL4 microkernel オペレーティングシステムのIsabelleによる検証も挙げられている。
HOL Lightを使ったthe Flyspeck project
- https://github.com/flyspeck/flyspeck
- https://www.youtube.com/watch?v=rE96vkzF01o
- https://www.youtube.com/watch?v=Is_lycvOkTA
証明スコアの変換： Conversion of HOL Light proofs into Metamath
以下にライブラリを構築するプロジェクト
QEDプロジェクト：
OpenTheoryプロジェクト：
MetaMathプロジェクト：
Mizar：
Coq：
Isabelle：
"Mixing Computations and Proofs" by Michael Beeson / July 18, 2014 のスライドは、
"the QED Singularity"が出てくる。
ビーソンのページ：
