Analysis I の Lean コンパニオン

 (terrytao.wordpress.com)
2 ポイント 投稿者 GN⁺ 2025-06-01 | 1件のコメント | WhatsAppで共有
  • Terence Tao が、実解析の教科書 Analysis I の定義・定理・演習問題を Lean コードに移すコンパニオンリポジトリを開始
  • 自然数・整数・有理数・実数の構成と集合論・論理を厳密に扱う教科書であるため、証明支援系で学ぶのに適した構造を持つ
  • 現在の範囲は第2章の一部と 3.1 の基本的な集合論、4.1 の 整数 までで、Mathlib の自然数との同型も含まれる
  • コードは Lean でコンパイルできるが、多くの sorry が残っており、公式解答の代わりにフォークで埋める方法が推奨されている
  • この資料は演習問題を Lean で解く代替ルートであると同時に、後半に進むほど Mathlib の使い方を学ぶ入門資料としても活用できる

Analysis I を Lean に移植するプロジェクト

  • Lean companion to “Analysis I” は、Analysis I のさまざまな定義、定理、演習問題を Lean に「翻訳」するプロジェクト
  • 書籍の演習問題は、Lean コード内の対応する sorry を埋める形でも解くことができる
  • 公式の演習問題解答はコンパニオンにはホストしない予定で、sorry を埋めたバージョンはリポジトリのフォークとして作成できる

教科書と Lean の相性がよい理由

  • Analysis I は、既存の実解析教科書を補完するため、基礎的な問題により重点を置いた教科書
    • 自然数、整数、有理数、実数の構成
    • 高い厳密性を持つ証明を展開できるようにする集合論と論理
  • 本を書いた当時、Coq や Agda のような証明支援系はすでに存在していたが、形式検証は当時の関心事ではなかった
  • その後、形式検証を経験する中で、本の内容が 証明支援系と相性がよい ことが確認された
  • 本で標準的な数体系を構成する際に暗黙に用いていた 素朴な型理論 は、Lean の依存型理論とよく合う
  • Lean の quotient type サポートも、本の構成方法とかみ合っている

現在 Lean に移植されている範囲

Mathlib との関係

  • 形式化は、一部では標準の Lean 数学ライブラリ Mathlib から分離され、別の箇所では Mathlib に依存するよう設計されている
  • Mathlib にはすでに標準的な自然数の概念がある
  • Lean での形式化では、まず自然数を「手で」再構成した Chapter2.Nat を開発する
    • Chapter2 名前空間で作業すると Nat として使用できる
    • Mathlib の自然数関連補題と並行する基本的な結果を設定する
    • これらの多くの証明は読者向け演習として残されており、現在は sorry で置き換えられている
  • エピローグの節では、この代替自然数と Mathlib の自然数 の間の同型を構築する
    • より正確には、その同型自体も演習問題として設定されている
  • 以降は第2章の自然数構成を使わず、Mathlib の自然数を使用する
  • 本の後半の章に進むほど、前章までの独自構成物よりも Mathlib の定義と関数 により多く依存するパターンを続ける予定

使い方と検証状況

  • リポジトリのコードは Lean でコンパイルできる
  • ただし、コード内の多数の sorry が実際にすべて埋められるかは、まだテストされていない
  • 必要な補題や Lean ファイルの API が十分かどうかも確認が必要
    • 目標は、難解な Lean プログラミング技法に依存しなくても、概念的に自然な形で sorry を埋められるかを確認すること
  • ボランティアがコンパニオンを プレイテストし、実際に Lean で演習問題を解けるか確認してくれることが望まれている
  • その他のフィードバックも歓迎されている

Lean・Mathlib 入門資料としての性格

  • このコンパニオンは実解析だけでなく、Lean と Mathlib の入門にも利用できる
  • この性格は Natural number game とある程度似ている
  • Natural number game は Analysis I の第2章とテーマ面で大きく重なる部分がある

関連記事

1件のコメント

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

  • 数学をLeanで教えるときに最も興味深い点は、即時フィードバックだと思う。学生の証明が間違っていれば、そのままではコンパイルされない。
    以前はTA、講師、専門家のような人に見てもらわないとフィードバックを得られなかったが、今ではLeanコンパイラが素早くフィードバックを与えられる。
    今後はRustコンパイラがコード修正の提案をしてくれるように、Leanコンパイラもより教育的なフィードバックを提供してくれるとよいし、おそらく専用のLLMが必要になるかもしれない。

    • ほぼ全面的に同意するが、証明の学習から遅い思考が抜け落ちる可能性がある点は気になる。
      以前の数学の勉強では、課題を前に紙の上であれこれ試しながら長く考え込む時間が多く、その過程が概念の内面化や新しい発想につながることもあった。
      Leanを使うと、やみくもに試してランダムに確認し、どんどん吐き出すようなやり方になることもあるのではないかと思う。Coqを何度か触ったときも、主にあれこれいじりながら試していた記憶が残っている。
    • Acornはすでにそのように動作する。証明に失敗したが「ほぼ合っている」場合、VS Codeで次のような提案を表示する。
      reduce(r.num, r.denom) = reduce(a, b)
      cross_equals(a, b, r.num, r.denom)
      r.denom * a = r.num * b
      LLMは使わず、VS Code拡張の中で小さなローカルモデルが動いている。いつかその小さなローカルモデルが人間をはるかに上回るほど強力になるといい。詳細はhttps://acornprover.org/docs/tutorial/proving-a-theorem/にある。

  • 本当に楽しみ。別リポジトリに移されて、見つけやすく他人に送りやすくなるとよい。
    もともと数学に興味があったが、TaoのAnalysisは、プログラミングする頭が期待していた厳密な形で数学がどのように構成されるのかを初めて見せてくれた教科書だった。
    その後Leanも少し触って、同じように満足感はあったが、Mathlibは数学の概念を学ぶ用途にはかなり複雑だった。だから本とツールをつなぐ橋ができるのはうれしい。

    • 私も収束やコーシー列のような内容をその本で学んだ。Hindustan Book Agencyという地域の非営利出版社から出ていて、価格も非常に安かった。

  • 解析学のような主流の数学分野で定理証明が勢いを増しているのを見るのはよい。
    プログラミング言語理論の分野では、2010年代半ばにはツールがかなり洗練され始めていた時期に、WinskelのThe Formal Semantics of Programming Languagesのような代表的教科書がIsabelleで形式検証されたことがある。完全な1対1の転写ではないが、http://concrete-semantics.orgがその例だ。
    定理証明に興味があるなら、個人的にはそちらのほうがはるかに簡単な出発点だと思う。解析学の定理はそれ自体がすでにかなり難しいからだ。

    • プログラミング言語の証明が入門用としてより簡単でも驚かない。人々が言うように、はるかに定型化された手順が多いように見える。
      構造的帰納法を行い、帰納法の仮定を適用して不変条件が保たれることを示し、そのまま進める、という具合だ。
      定理証明をたくさんやったわけでも、証明支援系で解析学のような「数学的」証明をしたわけでもないが、数学の証明がかなり別のアプローチを要求するなら、両者の間でどれだけスキルが移転するのか気になる。
      RocqのSoftware Foundationsにも触れておきたい。Leanへの移植があるかもしれないが、序盤を追ってみたときはかなり快適だった。

  • 主流の「教科書」的アプローチがMathlibのアプローチとどう違うのかを評価するのは、とても興味深そうだ。
    一般に形式化された数学ライブラリは、結果を可能な限り一般的に記述し、証明の展開をより直感的でエレガントにリファクタリングしやすくしてくれる。
    リファクタリングが容易なのは、何が何から論理的に従うのかをシステムが常に追跡しているからだ。紙とペンで作業しているとそれがないため、手直しの機会を逃すことが多い。
    学部課程でMathlib式の「最大限の一般性」版の実解析を教えるのが理にかなっているのかも、自然な問いだ。もちろん、証明ベースの数学の他分野についても同じことが言える。

    • 入門課程では、確実にそうではないと思う。すでに学ぶことが多すぎる。証明の仕方、プログラミングの仕方、そして本来の科目内容まである。
      実際に試した教員の経験も同様だと理解している。上級の学生にはよいが、平均的な学生にとっては授業時間を無駄にする可能性が大きい。
    • 数学者で、長年プログラミングもしてきた立場からすると、どんなプログラム的形式主義も基礎的理解を植え付けることには失敗しそうに思う。
      私の偏りは、数学の概念を論文から学んだことに由来している。
      コードは追加の負担が非常に大きく、たいてい何らかのスタイル基準にも従っていないことが多いと感じる。理解不能だと評される数学論文も読まなければならなかった者として言えば、コードには可読性の基準が事実上ほとんどないので、10倍はひどい。

  • Terence Tao本人のYouTubeチャンネルにも、Leanを使っている動画がいくつかある。https://www.youtube.com/@TerenceTao27
    詳しくは知らないが、LLMを使ったり使わなかったりしながら作業する様子を見るのはすばらしかった。

  • 解析学のような基礎的な分野には、とてもよいプロジェクトであり、よいアプローチだと思う。
    すぐに思い浮かぶ懸念は2つある。第一に、Mathlibの中核的な解析学の結果はフィルターの概念を使い、極限を一般的かつ統一的に扱う。それでも一部の結果はイプシロン-デルタ形式に特殊化されている。TaoのAnalysisは、より伝統的なイプシロン-デルタのアプローチを使うのだと思う。
    第二に、Mathlibは動きが速く、しばしば壊れる。名前が変わり、リファクタリングが続くため、下位リポジトリには継続的なメンテナンスが必要になる。

  • かなり急進的な考えだが、数学教育は Mathematica のようなコンピュータ代数システムや、Lean のような定理証明器を作ることに焦点を当てるべきだと思う。可視化や実用的な応用も強く取り入れるべきだ。
    極端に言えば、紙の上で数学をまったくやらなくても、学んだことすべてを Lean の中で証明できるようになる、という形かもしれない。
    今の体系は終わりのない手計算に集中しているが、あまりに役に立たなそうで退屈に見え、そのせいで人々が数学を嫌いになるのだと感じる。

  • Lean の教材とはいいね。ところで、なぜ HoTT はないのだろう？
    “Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
    https://news.ycombinator.com/item?id=43196452
    今週 HN に上がっていた追加の Lean 関連資料:
    “100 theorems in Lean”
    https://news.ycombinator.com/item?id=44075061
    “Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725

    • HoTT のさまざまなアイデアの形式化は、現在 Agda コミュニティで進められている。 https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/
      正確な動機は自分の分野外なので分からないが、Agda のほうが Lean よりもそれらのアイデアを形式化するのに適したやり方のようだ。
      今年後半には、既存の HoTT 本をより現代的に更新した新しい教材も出る予定で、Agda による形式化もある。
      https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
      https://github.com/HoTT-Intro/Agda
    • HoTT は非常に技術的で非常に狭いテーマなので、このように野心的なプロジェクトを2つ同時に扱うのは筋が通らない。
      HoTT は合理的な標準として受け入れられるにはまったく近づいておらず、ほとんどの人にとっては最初からつまずくテーマだ。
      JavaScript フレームワークの開発者に、なぜ Elm や Haskell 向けのフレームワークを作らなかったのかと尋ねるようなものだ。
    • なぜ HoTT があるべきなのかも分からない。
      HoTT の定理証明器を使いやすくするために投入された作業はずっと少なく、ドキュメントもはるかに貧弱だ。
      HoTT の利点も不明確だ。圏論の非常に難解な構成物を扱うときだけ、作業を減らしてくれるように見える。
    • 「なぜ HoTT がないのか」という質問は少し変だ。
      Terrence Tao には解析学の教科書が何冊かあり、これはその最初の本に対する Lean 伴走資料だ。彼は型理論の教科書を持っていないので、高次型理論がないというだけだ。そもそもやろうとしていることがまったく違う。
    • 既存の教科書に対する伴走資料であるという点だけでも、「なぜ HoTT ではないのか」への答えになる。別の理由としては、人々がその教育的価値を疑っているからかもしれない。

  • とても素晴らしい。Analysis I は、数学者ではなくエンジニアである自分が、Rudin のような他の本に何度も挑戦したあとで、初めて最後までついていきながら解けると感じた「本物の」数学教科書だった。
    Lean の伴走資料が、数学とプログラミングに慣れていて、厳密に学びたい人たちにとって、より取り組みやすいものにしてくれるといいと思う。

  • この数年、Tao の『Analysis I』を Lean で形式化しようとする試みは継続的にあり、いま Tao がやっていることとまったく同じことをしようとしていた人たちもいました。残念ながら、その多くは冒頭の数章を越えられませんでしたが、Tao にはさらに先まで進んでほしいところです
    私自身もやってみようかと考えたことがあります。私の『Analysis I』解説ブログ https://taoanalysis.wordpress.com/ に各練習問題の形式化された証明を付ければ、本に沿って学ぶ人たちに役立ちそうだと思ったからです
    本の非公開 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.lean に import Mathlib.Data.Set.Basic が見えるので、集合を新たに定義して公理を立てるというより、Lean の集合を取り込んでいるようです。このアプローチだと Lean が集合論について「知りすぎる」ことになり、目的にはあまり適さないかもしれません
    https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — 整数の構成用
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — 上と同じファイルかもしれません
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — 有理数の構成用
    https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — ユーザー定義の Set 型を定義する一つの方法を示しています