はじめてのCoq
「はじめてのCoq」再公開について
「はじめてのCoq」は、MaruLaboのハンズオンの資料として、2019年に公開されたものです。そのハンズオンの概要については、次のURLを見ていただければと思います。 https://coq-handson.peatix.com/
ChatGPTの登場は「人工知能」技術に対する関心を飛躍的に高めました。
その中で、言語ネイティブな人間に近いGPTのような大規模言語モデルに基づく「人工知能」技術とは異なる「人工知能」技術への関心も少しずつですが高まっているように思います。
Coq, Agda, Lean等は「証明支援システム」と呼ばれていますが、そのシステムとその背景にある「従属型理論」は、「推論する機械」-- いわば数学ネイティブな「人工知能」の構築を展望する上で、プリミティブですが最も基本的な出発点だと僕は考えています。
今回、3年前の資料を再公開したのは、Coqを多くの人に知ってもらうことは、意味があることだと改めて思ったからです。
( 残念ながら、現在(2023/06/11)、このページのビデオには音が入っていません。今時「無声映画」なんて！ 時間を見て「トーキー版」に作り替えますので、少しお待ちください。当面、このページのpdfの資料をご利用ください。）
(「音入れ」はじめました。が、当面、新旧混合のページになっています。すみません。Talkie版、タイトルを青くして横に表記しています。)
Coqのインストール
平原ゼミ Coq スタートアップセミナー を利用ください
Hands on のソース
Coq Tutorial https://github.com/maruyama097/coq-tutorial
旧ページのサイレントなムービーの再生リスト
新ページのTalkieなムービーの再生リスト
Hello Coq!
Coqとのはじめての対話 (Talkie)
( ムービー pdf blog:「ファースト・インプレッション」)
人間はCoqに何を伝えたか？ (Talkie)
( ムービー pdf blog:「証明することと証明を検証すること」)
Coqは人間に何を伝えたか？ (talkie)
( ムービー pdf blog:「「証明の状態」は変化する」 )
論理式の証明
論理式はどのような形をしているか？ (talkie)
( ムービー pdf blog:「論理学者は BARが好き」)
論理式の部分式への分解とサブゴール (talkie)
( ムービー pdf blog:「サブゴールはどこから生まれるか」)
