Analysis I の Lean コンパニオン

 (terrytao.wordpress.com)
2 ポイント 投稿者 GN⁺ 2025-06-01 | 1件のコメント | WhatsAppで共有
  • テレンス・タオが執筆した 実解析の教科書 Analysis I の中核内容を Lean 証明支援系に移し替えたプロジェクト
  • このプロジェクトは 基本的な数体系の構成 や証明論理など、厳密性を重視する原著の目標とよく合う構造を持つ
  • Mathlib 標準ライブラリを活用しつつ、主要概念を 自分で構築し、読者が自ら証明する練習 が含まれる
  • Lean コード上の空欄 (sorry) を自分で埋めながら練習でき、公式解説は提供されず、fork して拡張可能
  • Lean 初学者と実解析の学習者の双方 にとって、Mathlib と Lean の実際の活用法を体験する機会として有用

概要

  • テレンス・タオが書いた実解析の教科書 "Analysis I" を Lean 証明支援ツール で再構成したオープンソースプロジェクト
  • この教科書は、他の解析学の本と比べて 自然数・整数・有理数・実数の構成過程、およびその過程で必要となる集合論や論理的道具により重点を置いている
  • 本書の多くの部分は、体系的な 厳密な証明能力 の育成に焦点を当てており、Lean のような証明支援系と相性のよい構成になっている

Lean コンパニオンプロジェクトの特徴

  • 原著の定義・定理・練習問題を Lean 形式に「翻訳」して提供する
  • これらの Lean ファイルには、練習問題の解答に相当する 空欄 (sorry) が多く含まれており、それを読者が自分で埋める形で学習できる
  • 公式の解説（解答）は提供されないが、読者はリポジトリを fork して自分の解答版を作成できる

Mathlib との連携と差別化

  • Mathlib（Lean の標準数学ライブラリ）にすでに実装されている概念（例: 自然数）も、あえて別途自分で構築し、その後 Mathlib 版との同型性（等価性）を証明してみる過程 も用意されている
  • たとえば Chapter2.Nat では、Mathlib の自然数とは区別される独自定義の natural numbers を最初から構築し、主要な結果を自分で扱った後、最後に 2 つの版が同等であることを Lean 上で練習する
  • その後の章では、Mathlib の定義や機能を次第に多く活用していく流れになっている

学習と活用方法

  • この Lean コンパニオンは、解析学の学習だけでなく、Lean および Mathlib における数学の形式化方法への入門書 としての役割も果たす
  • "Natural number game" のように、Lean 環境で数学的対象を自ら定義し、練習してみられる構造化された演習が含まれる
  • コード自体は Lean でコンパイル可能だが、すべての練習問題（sorry）が実際に解けるかどうかは完全には検証されておらず、その意味でプレイテストとフィードバックが必要

オープンソースと貢献

  • リポジトリはオープンソースで、誰でも参照・fork・貢献できる
  • 公式ソリューションは別途提供されず、複数の解答バージョンの作成を支援する
  • 5月31日時点で、プロジェクトは 別個の独立リポジトリ に移行している

関連記事

1件のコメント

 
GN⁺ 2025-06-01
Hacker Newsの意見

  • このプロジェクトが独立したリポジトリに移されたら、他の人にも共有しやすく見つけやすくなるのではととても期待している。私は以前から数学に関心があり、TaoのAnalysisは、数学がどのように厳密に構成されるのかを自分のプログラミング的な思考様式に合う形で初めて示してくれた教科書だった。その後Leanにも夢中になったが、Mathlibで数学概念を学ぶには少し複雑だと感じていた。だから、本からツールへとつながる橋渡しをしてくれるこのプロジェクトが本当に気に入っているという話。

    • 私も似たような経験がある。収束やコーシー列などを学んだし、この本がインドの非営利出版社Hindustan Book Agencyから出ていて非常に安く入手できたことも懐かしく思い出した。

  • Leanを活用した数学教育で最もわくわくする点は、即時フィードバックが得られることだと思う。学生が証明を間違えればコンパイルが通らない。以前はTAや教授など人が直接フィードバックを与える必要があったが、今ではLeanコンパイラが素早く知らせてくれる。将来的にはRustコンパイラのように、より親切な修正提案まで出してくれる機能が加わってほしい（これには専用LLMの導入が必要かもしれない）。

    • 私も全体としてはほぼ同意するが、証明についてじっくり考える過程も重要だと思う。私の数学の経験はずいぶん昔のものだが、課題や問題を紙に書きながらゆっくり考える、いわば「数学の楽園」のような時間が多かった。Leanを使うと、むしろランダムに入力したり自動で通るまで試したりするような、手を動かすこと中心の流れになってしまうのではないかと心配している。昔coqを少し触ったこともあるが、ほとんどずっといじって試すだけになっていた記憶がある。結局のところtheorem solverは多くの面で有用だが、こうしたゆっくり咀嚼する過程が失われ、内面化や概念化、新しい発想が生まれる経路が弱くなるかもしれないという懸念がある。この点についてどう考えるか気になる。

  • Terence Tao本人がLeanを使う動画を見られる個人YouTubeチャンネルがあるという話。私はこの分野の専門家ではないが、LLMを使う場合も使わない場合も含めて、実際に作業している様子を見るだけでとても興味深かったという感想。 (https://www.youtube.com/@TerenceTao27)

  • 伝統的な「教科書的」アプローチをMathlib流のやり方と比較して評価するのは本当に面白そうだという考え。形式化された数学ライブラリは、一般にできるだけ一般的な形で結果を表現し、証明構造そのものをリファクタリングして優雅にしやすいという利点がある。リファクタリングは、システムが論理的依存関係を常に追跡してくれるので容易だが、紙とペンだけではそう簡単ではない。だから、Mathlibのような「最大限の一般性」版の解析学を大学講義で教えるのが妥当かどうかは自然な問題意識だと思う。これは他のすべての証明ベースの数学分野にも共通する悩みだという意見。

    • 少なくとも入門課程には向かないという立場。すでにカリキュラムには詰め込むべきものが多すぎる――証明法、プログラミングのやり方、そして基礎理論まである。実際に試した教授たちの経験も同様で、上級の学生にはよいが一般の学生には時間の無駄だという評価が多いと思う。

    • 私は長年プログラミングもしてきた数学者として、どんなプログラム的形式化も根本的な理解を育ててはくれないだろうと思っている。私の偏見は、概念を論文から学んできたことに由来する。コードはしばしばスタイルへの配慮がなく、可読性の面で圧倒されることがある。読みにくい論文ですら大変なのに、コードは標準もないので10倍つらいというのが個人的な経験だ。

  • theorem provingが解析学のような主流の数学分野でますます注目されているのはうれしいという感想。PLTではすでに、WinskelのThe Formal Semantics of Programming Languagesという代表的な本がIsabelleで形式検証された例があった。 (http://concrete-semantics.org) theorem provingを始めてみたいなら、そちらのほうが簡単でおすすめできると思う。解析学の定理はもともと難易度がかなり高いという補足もある。

    • PLの証明のほうが参入障壁が低いという話には私も驚かないと思う。ルーチン化された感じが強いとよく言われる――構造的帰納法、帰納法の適用、不変条件の証明、反復、といった流れだ。私はtheorem provingをあまり多くやったわけではないが、数学的な（特に解析学の）証明をtheorem proverで行ったことはない。「数学的」な証明はかなり違うアプローチを要求するのか、そしてその間でスキルがどれくらい移転するのかが気になる。参考までに、Software Foundations in Rocq（Leanへの移植があるかもしれない？）を勉強したことがあり、かなり楽しかった。

  • このプロジェクトとそのアプローチは、解析学のような基礎的な主題にとてもよく合っていると思う。ただし二つ懸念がある。

    1. Mathlibの解析学の中核結果はfilterの概念で統一的に扱われ、特殊な場合だけepsilon-delta型で別途扱われる。TaoのAnalysisはもっと伝統的なepsilon-deltaアプローチを取るだろうと予想される。
    2. Mathlibは変化の速いプロジェクトなので、名前や構造が常に変わる。連携情報は継続的に保守しなければならない。

  • とても素晴らしいプロジェクトだと思う。Analysis Iは、エンジニアである私が本当に初めて最後まで追いながら学べた「本物の」数学教科書だったし、他の本（Rudinなど）には何度も挑戦して失敗した経験がある。Lean版があれば、数学にもプログラミングにも親しみのある人たちが、概念をより厳密に学べるようになるのではと期待している。

  • TaoのAnalysis Iを公式にLeanで形式化しようとする試みはここ数年ずっと続いてきたが、いつも数章以上は進めるのが難しかったという事実。私も一時期この試みを自分でやりたいと思っていた。Analysis Iの解答ブログ（https://taoanalysis.wordpress.com/）に対応する形式化証明も一緒に載せれば、本で勉強する人たちにとって有用だろうと思っていた。すでに非公開Discordで整理した内容を共有したことはあるが、ここでは多くの人に役立ちそうな参考Leanプロジェクト（githubやgist、公式ドキュメントなど）へのリンクをまとめて共有する。

  • 「Mathlibに対応する対象との同型(isomorphism)の証明」が実際どれほど重要なのか気になる。もしかすると同型の部分を外しても、実質的には何も変わらないのではないか。たとえば定理の自動翻訳のようなことに実際使われるのだろうか？

    • こうした同型性の証明は、

      1. 自分で作った対象とMathlibにすでにある対象が本当に同じものだと証明できる。特にMathlib側では複雑に一般化された構成で定義されていることがあり、その違いを把握する助けになる。
      2. Mathlibでその対象を読み書きする際に使われる正式な記法や用語を理解するうえで決定的な役割を果たす。

    • 少なくとも教育的価値はあると思う。自分で構成した集合や演算が、本の別の場所でも「同じ」なのだと自分自身で納得する過程になるという意味で。

  • Leanベースの教科書が出てくるのはうれしい。だが、なぜHoTT（Homotopy Type Theory）はないのだろうか？ 「Type Theory(HoTT)が(ZFC)集合論を置き換えるべきか」という話題の記事もある。 (https://news.ycombinator.com/item?id=43196452) 今週HNに投稿されたLean関連の追加コミュニティリソースとして、「100 theorems in Lean」 (https://news.ycombinator.com/item?id=44075061) と、DeepMind Leanプロジェクト (https://news.ycombinator.com/item?id=44119725) も共有されている。

    • ただ、そこまでしてHoTTが必要な理由はわからない。HoTTのtheorem proverはまだ使い勝手が低く、ドキュメントも十分ではない。HoTTによる利点も明確ではなく、たいていは圏論のような極端に特殊な構造を扱うときにだけ意味があるという意見。

    • 従来の教科書スタイルだからこそ、「なぜHoTTではないのか」という問いにはすでに答えが含まれている。しかも教育効果について懐疑的な専門家も多いと思う。