授業の目的 【日本語】
Goals of the Course(JPN) | | |
|
授業の目的 【英語】
Goals of the Course | | The first part of the course (Bez) will cover the Brascamp-Lieb inequality
The second part of the course (Garrigue) will survey the foundations of proof assistants, such as AUTOMATH, Mizar, Isabelle, Coq/Rocq or Lean, which allow one to formally prove the correctness of theorems using computers.
The third part of the course (Hayashi) will cover Information-theoretic security. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN)) | | |
|
到達目標 【英語】
Objectives of the Course | | Part 1: To understand the fundamental theory of the Brascamp-Lieb inequality and some geometric applications
Part 2: Understanding the logical foundations and the differences between different approaches to computer-assisted mathematical proofs.
Part 3: Understanding the basics of information-theoretical security. |
|
|
授業の内容や構成
Course Content / Plan | | Part 1: The Brascamp-Lieb inequality
Lecture 1: The Loomis-Whitney inequality
Lecture 2: The Prekopa-Leindler inequality
Lecture 3: An introduction to the general Brascamp-Lieb inequality
Lecture 4: The geometric Brascamp-Lieb inequality
Lecture 5: The cube slicing problem
Part 2: Foundations of proof assistants (Garrigue)
The lectures will cover the different logical frameworks used by proof assistants, such as Tarski–Grothendieck set theory (Mizar), Higher-order logic (Isabelle), Type Theory (Coq/Rocq and Lean).
Part 3: Information theoretical security (Hayashi)
Lecture 1. Notations on probability theory
Lecture 2. Introduction of Information measure
Lecture 3. Security measure
Lecture 4. Hash function
Lecture 5. Leftover hashing lemma |
|
|
履修条件
Course Prerequisites | | Part 1: Undergraduate calculus and linear algebra. Knowledge of the Lebesgue integral will be useful.
Part 2: No requirement, but a basic knowledge of logic and set theory is useful.
Part 3: Undergraduate calculus and linear algebra. |
|
|
関連する科目
Related Courses | | Part 1: Undergraduate calculus and linear algebra
Part 2: Set theory
Part 3: Undergraduate linear algebra, Undergraduate calculus, Undergraduate probability |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | Grading is based on reports for the 3 parts.
The grade is based on the two best reports for each student. |
|
|
教科書・テキスト
Textbook | | |
|
参考書
Reference Book | | | Recommended books will be introduced in the lecture. |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | Review of each lecture is highly recommended. |
|
|
注意事項
Notice for Students | | |
|
他学科聴講の可否
Propriety of Other department student's attendance | | |
|
他学科聴講の条件
Conditions of Other department student's attendance | | | Ask the instructors first |
|
|
レベル
Level | | |
|
キーワード
Keyword | | Part 1: Brascamp-Lieb inequality, Loomis-Whitney inequality, Prekopa-Leindler inequality, Brunn-Minkowski inequality, cube slicing problem
Part 2: Theorem proving, Formal logic, Set theory, Type theory
Part 3: Information measure, information leakage, hash function |
|
|
履修の際のアドバイス
Advice | | |
|
授業開講形態等
Lecture format, etc. | | | Face-to-face lecture (+ TACT when necessary) |
|
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|