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

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

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

要申込： 6月17日（水）締切厳守！
※講義は対面で行います。受講希望者は、KULASIS「お知らせ」内のGoogleフォームにて申し込みを行ってください。聴講のみの希望者も申し込みが必要です。