授業の目的 【日本語】
Goals of the Course(JPN) | | | 数学者は現在、定理証明支援系を用いて計算機で証明の検証を行っている。本講演の目的は、組合せ論、代数学、実解析などの証明の検証に使用されてきたMathematical Componentsライブラリを入門することである。 |
|
|
授業の目的 【英語】
Goals of the Course | | | Mathematicians are now using proof assistants to check their proofs with a computer. The goal of this lecture is to introduce the Mathematical Components library, an extension of the Coq proof assistant that has been used to verify mathematical proofs in combinatorics, algebra, and analysis. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN)) | | この授業では，受講者が授業終了時に，以下の知識・能力を身につけていることを目標とする。
1. 形式論理による数学の言明を読み書きできる。
2. Mathematical Componentsを用いて数学の型式検証を行うことができる。
3. 定理を検証するため、必要な定義や補題の理論を設計することができる。
4. 形式検証の共同作業に参加することができる。 |
|
|
到達目標 【英語】
Objectives of the Course | | 1. The student is able to read and write mathematical statements in formal logic
2. The student is able to carry out a formal proof using Mathematical Components
3. The student is able to design a theory of definitions and lemmas to verify a theorem
4. The student is able to participate in a collaborative effort of formal verification |
|
|
授業の内容や構成
Course Content / Plan | | 本講義では、 測度論という具体例を用いて、Mathematical Componentsライブラリをチュートリアルとして行う：
1. 定理証明支援系Coqを用いた形式論入門
2. Mathematical Componentsライブラリの紹介
3. 集合論と位相幾何学の形式化
4. 収束と測度論の形式化
5. ルベーグ積分の型式化
The lecture consists in a tutorial about the Mathematical Components library using measure theory as a running example.
1. Introduction to formal logic proof using the Coq proof assistant
2. Introduction to the Mathematical Components library
3. Formalization of naive set theory and topology
4. Formalization of convergence and measure theory
5. Formalization of Lebesgue integration |
|
|
履修条件
Course Prerequisites | | プログラミングと測度論の基礎知識。関数型プログラミングや形式論理の経験・興味があること。
Basic knowledge of programming and of measure theory.
Experience with functional programming and formal logic may help.
この講義は英語で行います。
This course will be taught in English. |
|
|
関連する科目
Related Courses | | | 2021年度秋・数理解析・計算機数学 IV (同 概論IV) |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | 定理や理論を型式化し、その結果をコメント付きのCoqファイルとして提出すること。グループワークを推奨する。宿題期間中は、講師がオンラインで指導できる。
The student is expected to formalize a theorem or a theory, and to submit a commented Coq file as a report. Group work is recommended. The instructor is available to help during the homework period. |
|
|
教科書・テキスト
Textbook | | 講義中に講師がpdf資料を提供する
pdf material to be provided by the instructor during the lecture |
|
|
参考書
Reference Book | | 森北出版, 2018
- Assia Mahboubi and Enrico Tassi,
Mathematical Components,
Zenodo, 2021,
https://doi.org/10.5281/zenodo.4457887
- Georges Gonthier, Assia Mahboubi, and Enrico Tassi,
A Small Scale Reflection Extension for the Coq system,
Inria RR-6455, 2016,
https://hal.inria.fr/inria-00258384v17/file/main.pdf
- The Coq Proof Assistant Reference Manual,
The Coq Development Team,
Inria, 2022,
https://coq.inria.fr
- Yves Bertot and Pierre Casteran,
Interactive Theorem Proving and Program Development---Coq'Art: The Calculus of Inductive Constructions,
Springer, 2004
- Yves Bertot and Pierre Casteran,
Le Coq'Art (V8), 2015,
https://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf (in French) |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | |
|
注意事項
Notice for Students | | |
|
他学科聴講の可否
Propriety of Other department student's attendance | | |
|
他学科聴講の条件
Conditions of Other department student's attendance | | |
|
レベル
Level | | |
|
キーワード
Keyword | | 型理論、定理証明支援系、型式論理、関数型プログラミング、測度論、実解析
Type theory, proof assistant, formal logic, functional programming, measure theory, analysis |
|
|
履修の際のアドバイス
Advice | | |
|
授業開講形態等
Lecture format, etc. | | |
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|