解析の定理証明実践＠Lean 4

Proof Summit 2025の発表スライドです

Transcript

1. 解析の定理証明実践 ＠Lean 4 by dec9ue
2. 自己紹介 • @dec9ueと言います • 普段はものづくりに関わったり、 • システム設計してみたり • 学生でもある X : https://x.com/dec9ue Zenn : https://zenn.dev/de9ue
3. 目指していること • 常微分方程式を含むシステムの性質を検証して モノの検証に活かしたい • ひとまず、なんでも検証できるLeanで書いてみる • 日々、消しては書き消しては書き、、、
4. 今日話すこと • Lean初心者として普段の証明の環境について共有 • 日々の鬱屈を共有し、より良い環境を目指したい • 普段Lean使っている方にはあまり新情報はないか も。。。
5. Leanで数学証明を書く環境
6. 普段使っている 環境 • VS Code + Lean 4 Extension • GitHub Copilot ※これだけ。 使っている環境 • Lean本体／ビルドツールlake • Extension経由で実施 • 数学ライブラリMathlib • プロジェクトをlake buildすると勝手に落ちてくる • 数学プロジェクトの作り方 • lake new <my_project> math インストール作業など
7. Leanの環境に ついて、感想 良き点 • インストール超楽。 • 理論的にシンプルに感じる。CICのおかげ？ • マテリアルはある。 • サポート意思のある日本人が多いかも。 • 数学証明を書きやすい。（記法など） 悪き点 • 導入が簡単すぎて中身がよくわかってない。 • よくない点はまだよくわからない、かも。
8. 数学証明を 始めた人の難しさ • とにかくライブラリ体系が把握しきれない • 応用問題になればなるほど、たくさんの数学分野と の関係が必要になる • それぞれがLeanでどのように形式化されているの か、膨大すぎて把握できない
9. Lean Mathlib Fundamentals, Duality, Finite-dimensional vector spaces, Finitely generated modules over a PID, Matrices, Endomorphism polynomials, Structure theory of endomorphisms, Bilinear and quadratic forms, Finite-dimensional inner product spaces Linear algebra General topology, Uniform notions, Topological algebra, Metric spaces Topology Topological vector spaces, Normed vector spaces/Banach spaces, Hilbert spaces, Differentiability, Convexity, Special functions, Measures and integral calculus, Complex analysis, Distribution theory, Fourier analysis Analysis Definitions in probability theory, Random variables and their laws, Convergence of a sequence of random variables, Stochastic Processes Probability Theory Affine and Euclidean geometry, Differentiable manifolds, Algebraic geometry Geometry Graph theory, Pigeonhole principles, Transversals Combinatorics Circle dynamics, General theory Dynamics List-like structures, Sets, Maps, Trees Data structures Computability, Set theory, Model theory Logic and computation Category theory, Numbers, Group theory, Rings, Ideals and quotients, Divisibility in integral domains, Polynomials and power series, Algebras over a ring, Field theory, Homological algebra, Number theory, Transcendental numbers, Algebraic Number Theory, Representation theory General algebra https://leanprover-community.github.io/mathlib-overview.html より構成
10. VS Code Extension • Lean本体のインストールができる • ステート表示をしてくれる • インポート先ライブラリを含めた シンボル補完ができる これなしに生きてはいけない。。。
11. GitHub Copilot • Inline completion • 書き途中の証明を見て良さそうなサ ジェストを出してくれる • 間違っていれば無視すれば良い • Copilot Chat • 証明方針をAIに相談したいときはこれ • いい時もあれば、悪い時も • 最近の自分はClaude 3.7 Thinking • GPTはLean 3の定理を返す傾向を感じ る 証明方針のサジェスト
12. タクティクの活用 • exact? • 現在のゴールを「締める」定理をピックアップ • 頭が思考を拒否した時に便利 • apply? • 現在のゴールを分解する定理をピックアップ • 数学の定理証明には？？？ • simp? • simpで解けた時に、使った定理だけに絞ってくれる • 中間simpは特にお行儀が良くないので、改善に使え る • 「改善ができるからsimpを叩いて良い」という自分 への言い訳に使える
13. 検索の活用 • Loogle • 型や名前からLeanシンボルを検索 • Moogle • 自然言語でのLeanシンボル検索 • いい感じに探してくれる…のを期待
14. 普段使っている道具たちまとめ カテゴリ 機能 感触 効用と感想 VS Code Extension 証明ステート表示 ◎ なしで生きられない シンボル補完 ◎ GitHub Copilot Inline completion ◦ 比較的自分の直感に近いサジェスト コピペ証明を増やすという意味では悪？ Copilot Chat ◦ 証明方針自体のサジェストに使える ただし、GPTのサジェストにはLean3の 定理が混じることが多く感じる タクティク exact? ◎ SMT Solver等による証明支援 頭が思考を拒否した時に助けてくれる simp? ◎ apply? 数学の証明ではあまり役に立たず 検索 Loogle: シンボル検索 △ 型情報などから広くシンボルを検索 Moogle: AI検索 役に立った記憶が全くない
15. 実践的に常微分方程式を解いていく
16. 常微分方程式を 解いて解の性質を 調べる • 常微分方程式を解くために、Cauthy-Lipschitzの定 理がそのまま使える • 𝑓に関する常微分方程式の解が𝑔であることを示せる 閉区間[𝑎, 𝑏]において、 𝑓 𝑡 , 𝑔 𝑡 は連続かつ 𝑑𝑓 𝑑𝑡 = 𝑣 𝑓 𝑡 , 𝑡 かつ 𝑑𝑔 𝑑𝑡 = 𝑣 𝑔 𝑡 , 𝑡 𝑣 𝑥, 𝑡 はLipschitz連続かつ、 𝑓 𝑎 = 𝑔(𝑎) ならば、 閉区間[𝑎, 𝑏]において、 𝑓 𝑡 ＝𝑔 𝑡
17. フィルターで 極限を示す • 二つのtrivialな定理の例 • lim 𝑥→∞ 𝑓 𝑥 = 0 ならば lim 𝑥→∞ 𝑐 ∗ 𝑓 𝑥 = 0 • lim 𝑥→∞ 𝑓 𝑥 = 0 ならば lim 𝑥→∞ 𝑓 𝑥 /𝑐 = 0 • Tendsto f atTop (𝓝 v) はおおまかに lim 𝑥→∞ 𝑓 𝑥 = 𝑣 を表す • atTopは𝑥 → ∞を表すフィルター、(𝓝 v)はvの近傍
18. 関数の有界性を 示す • lim 𝑥→∞ 𝑓 𝑥 = 𝐾となる連続関数𝑓の有界性 • [0, 𝑇]と[𝑇, ∞)に分割 • 前者はコンパクト性から、後者は収束性から有界 (中略) という初等的証明を普通に書ける
19. まとめ
20. まとめ • Leanの定理証明は簡単に導入できて結構手厚い！ • 定理がわかっていなくても、ある程度はシステムに 頼れる • しかし意外にMoogleが役に立たない（個人の感 想） • Mathlibは数学表現をそこそこ素直に書ける