定理証明支援系 Lean と生成AIを組み合わせて数学の定理を自動証明する試みが世界で活発に行われている。2026年の年明けには、Erdős問題をはじめとする未解決問題まで解決できるようになってきた。今日の AI は統計的な学習に基づく乱数生成器であるから、原理的に幻覚（hallucination）を起こしやすい。AIが生成する大量の「証明もどき」を機械的にフィルタリングする技術として、Lean のような形式検証システムを組み合わせる方法は、今後急速に普及していくものと考えられる。

本講義では、数学系の大学院生を念頭において、定理証明支援系 Lean を用いた形式証明の入門的講義を行う。まず、証明の正しさを機械的に検査する形式証明の考え方を紹介する。続いて Lean の基本的な記法とシステム構成を学び、最終的に学部レベルの数学（微積分や線形代数など）の初歩的な内容を Lean 上で証明するところまでを目指す。プログラミング理論や数理論理学、証明論等の踏み込んだ知識を前提とせず、一般のエンドユーザーとして向き合えるようになることを目指す。

この講義は、高度に専門的な予備知識を仮定せず、代数・幾何・解析などの分野にかかわらず広く修士課程の大学院生や学部生に開かれた講義として用意されたものですので積極的に受講してください。

申込締切： 6月17日（水）締切済

【教室変更のお知らせ】
6月22日（月）15時〜17時 　理学研究科 6号館301号室
6月23日（火）15時〜17時 　理学研究科 6号館301号室
6月24日（水）10時〜12時 　理学研究科 3号館110号室　
6月25日（木）15時〜16時30分 　理学研究科 6号館301号室
6月26日（金）15時〜17時 理学研究科 　 6号館401号室（変更の可能性あり）