檜山正幸のキマイラ飼育記 メモ編 このページをアンテナに追加 RSSフィード

キマイラ・サイト
キマイラ飼育記 本編
メモ編のアーカイブ
檜山の公開プライベート(なんじゃそりゃ?)メモ
檜山本人以外の読者を考慮しておりません。あしからず。

hiyama{at}chimaira{dot}org

2017-08-11(金)

QEDマニフェスト/QEDプロジェクト

| 15:04

"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

証明スコアの変換: 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"が出てくる。

ビーソンのページ:

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20170811/1502431494