分析Iのためのリーンコンパニオン

359日前原文(terrytao.wordpress.com)

概要

Analysis I の内容を Lean で形式化したコンパニオンの紹介
自然数や集合論 など、基礎的な構成と証明をLeanで再現
Mathlib との連携と独自定義の使い分け方針
演習問題 はLeanの“sorries”として実装し、解答は利用者に委ねる設計
Lean/Mathlib学習 や 実分析入門 としても活用可能

「Analysis I」Leanコンパニオンの概要

約20年前に執筆した実解析教科書 “Analysis I” の内容を、 Lean による形式化で拡張
自然数・整数・有理数・実数の構成、集合論・論理など、基礎理論の厳密な証明力を重視
当時は Coq や Agda 等の証明支援系は認識していなかったが、現在Leanとの高い親和性を実感
書籍内の定義・定理・演習問題を Leanコード へ“翻訳”し、演習は“sorries”を埋める形で実施可能
公式解答 は提供せず、各自でリポジトリをフォークして“sorries”を埋める運用を推奨

Leanへの翻訳済みセクション

Section 2.1: 自然数の構成
Section 2.2: 加法
Section 2.3: 乗法
Chapter 2 Epilogue: Mathlib自然数との同型性
Section 3.1: 基本的な集合論
Section 4.1: 整数の構成

Mathlibとの連携・独自定義の方針

一部は Lean標準ライブラリMathlib に依存しつつ、一部は独自に定義
例： 自然数 はまず独自にChapter2.Natとして構成し、基本的な補題を証明（多くは演習として“sorries”で残す）
エピローグで Mathlib自然数 との同型性を示し、以降はMathlibの定義・関数を使用
このパターンを全章で踏襲し、進行とともに Mathlib依存度 を高める設計
Lean/Mathlibの導入教材 や実解析入門としても利用可能（“Natural number game”とテーマが重なる部分あり）

利用・参加の呼びかけ

Leanコード はコンパイル可能だが、“sorries”が全て解けるかは未検証
ボランティアによる“プレイテスト” を募集中
- 補助補題やAPIが直感的に“sorries”を埋めるのに十分か、Lean特有の難解な技法を要しないか等のフィードバック歓迎
その他のフィードバック も随時受付

更新情報

2024年5月31日: コンパニオンを 独立リポジトリ へ移動

Hackerたちの意見

これめっちゃ楽しみ！独立したリポジトリに移してもらえると、探しやすくて他の人に送るのも楽になると思う。数学にはずっと興味があって、タオの『解析』が初めて、プログラミング脳が求めてた厳密な構成の仕方を教えてくれた教科書だった。それからちょっとLeanにも手を出したけど、同じように満足感があったけどMathlibは数学の概念を学ぶにはちょっと複雑なんだよね。だから、この本からツールへの架け橋が見えるのは嬉しいな。

└

同じく！収束やコーシー列について学んだんだけど、地元の非営利出版社であるヒンドスタンブックエージェンシーから出版されてたから、すごく手頃だったよ。

この「Mathlibと同等の同型を証明する」って、どれくらい重要なんだろう？同型の部分が抜けても何か変わるのかな？例えば、自動的に定理を翻訳するために使われてるとか？

└

何もないにしても、教育的な価値はあるよね。自分が確立した集合や演算が、本の他の部分で使ってるものと「同じ」だって納得できるから。

└

https://taoanalysis.wordpress.com/

定理証明が解析みたいな主流の数学トピックで勢いを増してるのを見るのはいいね。PLTでは、2010年代中頃にIsabelleを使って（まあ、1対1の転写ではないけど）正式に検証されたフラッグシップの本（ウィンスケルの『プログラミング言語の形式意味論』）があったし、ツールがかなり洗練され始めた頃だった。個人的には、定理証明に興味があるなら、そっちの方がずっとシンプルなスタート地点だと思う。解析の定理はそれ自体でかなり難しいからね。

└

PLの証明が最初はもっと簡単だったとしても、あんまり驚かないな。みんなが言ってるのは、ルーチン的な部分が多いからってこともあるみたい。構造的帰納法を使って、帰納法の仮定を適用して不変条件が成り立つことを示して、あとは続けるだけ。俺はあんまり定理証明をやったことがないし、「数学的な」証明（例えば解析学）を定理証明器でやったこともないけど、もし「数学的な」証明が全然違うアプローチを必要とするなら、どれくらいスキルが移転するのか気になるな。あと、RocqのSoftware Foundationsも言っとくね（もしかしたらLeanのポートがあるかも）。最初の部分をいくつかやってみたけど、結構楽しかったよ。

主流の「教科書」アプローチとMathlibのアプローチを比較するのはすごく面白いと思う。一般的に、形式化された数学ライブラリは、結果を最大限の一般性で述べるのが比較的簡単で、証明の発展を簡潔さや優雅さのためにリファクタリングするのも楽になる。リファクタリングが簡単になるのは、システムが論理的に何が何に続くかを常に追跡してくれるから。ペンと紙で作業してるとその感覚がないから、再作業の機会がしばしば無視されちゃう。Mathlibの「最大一般性」版の実解析を教えるのが意味があるのか、あるいはそれに近いものを学術コースで教えるのがいいのかっていうのも自然な疑問だよね。他の証明ベースの数学の分野でも同じことが言えるけど。

└

数学者で、プログラミングも結構やってきた私としては、プログラム的な形式主義は根本的な理解を育むのには失敗すると思う。私のバイアスとしては、数学的概念を学術論文で学んできたからね。コードが提示するオーバーヘッドは膨大だと感じるし、スタイルに関してはほとんど遵守されてないことが多い。理解不能とされる他人の数学論文を解析しなきゃいけなかったことがあるから、こう言ってるんだ。コードはそれよりも10倍ひどい。理解可能性に関する基準がほとんどないからね。

└

入門コースには絶対向いてないね。すでにやることが多すぎる - 証明の仕方、プログラミング、そして基本的な教材自体。教員たちも同じような経験をしてると思うけど、上級者にはいいけど、普通の生徒には授業時間の無駄だよね。

Leanを使って数学を教える一番の魅力は、即時フィードバックだと思う。もし学生の証明が間違ってたら、コンパイルすら通らないからね。以前は、学生が受け取れるフィードバックはTAや講師、他の知識のある専門家からのものだけだった。でも今は、Leanのコンパイラから迅速なフィードバックが得られる。将来的には、Rustのコンパイラがコードの修正を提案するように、Leanのコンパイラからももっと指導的なフィードバックが得られるオプションがあればいいなと思ってる。（でも、これには専用のLLMが必要になるだろうけど。）

└

これにはほぼ完全に賛成だよ。でも、証明することについても考えてる。自分の数学の経験は数十年前のことだけど、課題をじっくり考える時間をたくさん過ごしたんだ。紙の上で色々試したり、煙草の煙やコーヒーに浸ったり、基本的な数学パラダイスみたいな感じ。ここでLeanを使うことで、もしかしたら無駄に手探りしたり、ランダムにチェックしたり、思いつきを口にすることになるんじゃないかって心配してる。Leanはあまり使ったことがないけど、5年か10年前にcoqを少し触ったことがある。記憶では、ほとんどいじってみたり試してみたりした感じ。結局、ソルバーは色々なことに役立つかもしれないけど、このじっくり考えるやり取りが内面化や概念化、時には新しいアイデアにつながることを妨げるんじゃないかって思う。これについてどう思う？

Leanの教科書だ！でもHoTTはなんでないの？「タイプ理論（HoTT）は数学の基礎として（ZFC）集合論に取って代わるべきか？」 https://news.ycombinator.com/item?id=43196452 今週のHNからのLeanの追加リソース：「Leanでの100の定理」 https://news.ycombinator.com/item?id=44075061 「Google-DeepMind/formal-conjectures: Leanで形式化された予想のコレクション」 https://news.ycombinator.com/item?id=44119725

└

でもなんでHoTTが必要なの？HoTTの定理証明器を使いやすくするためにかけられた労力はずっと少ないよ。それに、ドキュメントもかなり少ないし。HoTTの利点も不明瞭だし、カテゴリー理論のすごく難しい構造を扱うときにしか労力を節約できないみたい。

└

これは既存の教科書で、「なんでHoTTじゃないの？」って質問に答えてるよ。ただ、もう一つの理由は、その教育的価値に疑問を持つ人がいるかもしれないね。

彼はLeanを使ったいくつかの動画があるYouTubeチャンネルも持ってるよ [1]。あんまり詳しくは知らないけど、彼がLLMを使ってるのを見たり、使ってないのを見たりするのは面白かった。 [1] https://www.youtube.com/@TerenceTao27

すごくいいね。解析学は、俺（エンジニアで数学者じゃない）が他の教科書（ルーディンとか）を何度も試みた後に、やっと完全に理解できて進められた「本物」の数学の教科書だった。Leanのサポートがあれば、数学やプログラミングに慣れた人たちがもっと厳密に学べるようになるといいな。

これはすごくいいプロジェクトだし、解析学のような基礎的なテーマに対してすごく良いアプローチだと思う。いくつかの心配事があるけど：1. Mathlibのコアな解析結果は、フィルターの概念を使って一般的で統一的な方法で極限を扱ってる。でも、これらの結果にはε-δ形式への特別な適用もあると思う。多分、タオの解析学はもっと伝統的なε-δアプローチを使ってるんじゃないかな。2. Mathlibはすごく早く進化して、壊れてしまうことがある。名前が変わったり、リファクタリングされたりすることがよくあるから、下流のリポジトリは常にメンテナンスが必要だよ。

└

自分で見てみて。実数列の極限に関する章の多くがサンプルページに載ってるよ。ここを見てみて： https://link.springer.com/chapter/10.1007/978-981-19-7261-4_...

年々、Taoの『Analysis I』をLeanで形式化しようとする人たちが絶えず現れてるね。つまり、今Taoがやってることをそのままやってるわけ。残念ながら、彼らは最初の数章を超えられないんだけど、Taoにはもっと進んでほしいな！自分もこれをやろうか考えてたんだ。そうすれば、自分の『Analysis I』の解答ブログに各演習の形式化された証明を添えられるから（本を進めてる人には役立つかなと思って）。以下の内容を本のプライベートDiscordサーバーに投稿したんだけど、ここで共有するのもいいかもと思った。誰かに役立つかもしれないしね：

https://github.com/cruhland/lean4-analysis （https://github.com/cruhland/lean4-axiomaticから引っ張ってる）
https://github.com/Shaunticlair/tao-analysis-lean-practice
https://github.com/vltanh/lean4-analysis-tao
https://github.com/gabriel128/analysis_in_lean
https://github.com/mk12/analysis-i
https://github.com/melembroucarlitos/Tao_Analysis-LEAN
https://github.com/leanprover-community/NNG4/ （これはTaoの本に従ってないけど、自然数のゲームのLean4版だから、第2章と似た内容がある）
https://github.com/djvelleman/STG4/ （前のやつと似てて、Lean4の集合論ゲームだから、第3章と似た内容かも。ただ、https://github.com/djvelleman/STG4/blob/main/Game/Metadata.l... で「import Mathlib.Data.Set.Basic」ってあるから、これは新たに定義するんじゃなくて、Leanから集合をインポートしてるみたい。だから、このアプローチだとLeanが集合論について「知りすぎる」ことになり、私たちの目的には良くないかも）
https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c... -- 整数を構築するためのもの
https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2... -- 上のファイルと同じかも
https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2... -- 有理数を構築するためのもの
https://lean-lang.org/theorem_proving_in_lean4/axioms_and_co... -- カスタムセット型を定義する方法の一つを示してる

ハクソク