数学者がLean Theorem Proverについて知っておくべきこと：信頼性とAI

私の研究や解説論文の最新情報、未解決問題の議論、その他の数学関連トピック。 ホーム プロフィール キャリアアドバイス 執筆について 書籍 Mastodon + アプレット フィードを購読する 数学者がLean Theorem Proverについて知っておくべきこと：信頼性とAI 2026年10月9日 in math.GM, opinion | タグ: AI, Lean, Thomas Hales | 投稿者: Terence Tao [これはThomas Hales氏によるゲスト投稿です。このブログ記事は元々異なるファイル形式で書かれており、AIを使用して変換されました。 — T。] 数学者たちは、数学の価値について意見を表明してきました。私にとって重要なのは、数学の一貫性と、科学および文明を支える比類なき信頼性です。 数学の形式化 形式的証明とは、数学の基礎と論理の基本規則のレベルで徹底的に検証された数学的証明のことです。理論的には手作業で行うことも可能ですが、ステップ数が膨大であるため、通常はこのタスクのために設計されたソフトウェアを使用してコンピュータで行われます。形式化された定理の例としては、四色定理、Feit-Thompson（奇数階）定理、ケプラー予想、球体の外転、8次元および24次元における球充填問題、Navier-Stokes強制吹き上げ、そしてフェルマーの最終定理があります。最後の3つの形式化プロジェクトは今年完了し、形式化の可能性について広く認識されるようになりました。 形式化のためのソフトウェアシステムは、証明支援系、定理証明器、または対話型定理証明器などと呼ばれます。この記事では、これらの用語は同義語として使用します。長年にわたり多くの証明支援系が開発されてきました：Automath、HOL Light、Isabelle、Coq（昨年Rocqに改名）、Metamath、Mizar、そしてLeanです。Freek Wiedijkは、これらの証明支援系の一部を比較した書籍「The Seventeen Provers of the World」を編集しており、それぞれで√2の無理数性の証明を行っています。数学者の間では、Lean定理証明器が最も人気があり、この記事ではLeanに焦点を当てます。 Leanは2013年にLeo de Mouraによって開発・導入されました。彼はMicrosoftに在籍していました。彼の多大な貢献により、Microsoftはこのソフトウェアをオープンソース化しました。Jeremy Avigad（カーネギーメロン大学の新しいNSF研究所ICARMのディレクター）は、Leanの最初のユーザーであったと、Kevin HartnettはLeanの歴史に関する著書「The Proof in the Code」で述べています。私は2015年に彼が開催したLeanセミナーに参加しました。2017年、Jeremyの大学院生の一人であるMario Carneiroは、Johannes Hölzlと協力して、Leanのコアライブラリの既存部分を取り出し、mathlibと呼ばれる別のLean数学ライブラリを開始しました。この形式化された数学のライブラリは現在巨大で、約30万の定理、10万以上の定義、250万行のコードを含み、700人以上の貢献者がいます。mathlib内の任意の定義または定理を使用して、さらなる定理を証明できます。例えば、コーシー・シュワルツの不等式を使用する証明では、結果を再証明するのではなく、ライブラリから引用できます。 自動形式化は現実のものとなっています 過去には、研究者は紙の証明を形式的証明に手作業で転写する必要がありました。例えば、3次元におけるケプラー予想の球充填に関する形式的証明は、約20人年の作業を要し、約50万行の証明スクリプトで構成されていました。長年、形式化に携わる多くの人々にとって、プロセスに自動化を増やす方法を見つけることが夢でした。自動形式化は、その夢の実現です。自動形式化とは、AIによる数学の形式化です。AIは論文（PDFまたはtexファイルなど）を読み込み、Leanまたは他の証明支援系で形式的証明を出力します。自動形式化は2026年に現実のものとなりました。2025年の晩春から夏にかけて、研究者たちは自動形式化についてますます楽観的になっていました。以下にいくつかのマイルストーンを示します。 2025年9月、Math Inc.は素数定理の準自動形式化を生成しました。このプロセスは「準」に過ぎませんでした。なぜなら、AIが行き詰まった場合に人間がさらなるガイダンスを与える必要があったからです。 2026年1月、J. UrbanはarXivのプレプリント「130k lines of formal topology in two weeks」を投稿しました。これは、集合論に基づいた証明支援系で、Munkresのトポロジー教科書の大部分を自動形式化しました。 2026年3月。8次元における形式化完了を発表してから約1週間後、Math Inc.は、Viazovskaとその共同研究者による証明に続いて、24次元における球充填問題の自動形式化を発表しました。このプロジェクトは、約50万SLOC（ソースコード行数）を生成し、ゴルフ（またはコードの枝刈り）によって後に約20万行に削減されました。 2026年5月、Meta/Facebook Researchのグループは、ATLASと呼ばれるプロジェクトで26冊の数学教科書の大部分を自動形式化しました。そこから、数多くの定理が自動形式化されました。特に注目すべきは、9月4日にAnthropicが発表したフェルマーの最終定理の自動形式化です。このプロジェクトは11日間で1300万行のLeanコードを生成しました。9月8日にOpenAIが発表した強制を伴うNavier-Stokes吹き上げの発表には、Leanにおける定理の自動形式化が伴いました。 今後について、Urbanは1月に「（自動）形式化は、どの証明支援系が使用されるかに関わらず、2026年には非常に簡単で遍在するものになると信じています」と述べています。自動形式化プロジェクトは、さまざまなLLMを使用してさまざまな証明支援系で完了していますが、私たちはLeanに焦点を当てます。「Jesse Hanにとって、それはさらに多くのことを意味します。極めて大規模な形式化が一般的になる数学における革命的な変革の始まりです」（IEEE Spectrum）。Jared Lichtmanは2026年9月8日にMAP（Mathematics Autoformalization Project）の立ち上げを発表しました。これは「すべての既知の数学を形式コードに翻訳する」ことを目的としています。彼は、次の1兆行のコードを想像するように求めています。 Leanは信頼できますか？ 型理論。 Leanは型理論、実際にはCIC（calculus of inductive constructions）と呼ばれる型理論の特定の弁証法に基づいています。この記事は型理論のチュートリアルを意図したものではなく、簡潔にします。ラッセルの有名なパラドックス（1901年）は、数学の基礎に危機をもたらしました。その十年後、2つの解決策が提案されました。(1) 安全でない集合の作成を禁止するZermeloの公理系。(2) ラッセルパラドックスのような実体を生成することを構文エラーとする型理論。型理論は、1903年にラッセル自身が著書「Principles of Mathematics」で導入し、ラッセルとホワイトヘッドの「Principia」の基礎システムの一部となりました。集合論に慣れている数学者にとって、B. Wernerの論文（1997）「Sets in Types, Types in Sets」は、集合論で行ったことは型理論に翻訳でき、型理論で行われたことは集合論に逆翻訳できることを保証します。より正確には、この論文はZFC集合論がCICにエンコードでき、CICの特定の弁証法がZFC（到達不能基数階層で補強された）に逆エンコードできることを示しています。問題をあまりにも単純化しすぎるリスクを冒して、私たちは「型は互いに素な集合のようなもの」であり、型理論の各要素は「ちょうど1つの型に属する」要素であると言えます。自然数2の型は自然数型です。自然対数の底eの型は実数型です。そしてその逆も同様です。自然数型は実数型とは互いに素であり、明示的な強制（2を2.0に送る）が自然数型から実数型に構築されます。講演をするとき、私は集合を非空共通部分を持つベン図として、型を互いに交差しない積み重ねられたレンガの画像として描くことがあります。 Leanの設計 Leanシステムの一部は、汎用プログラミング言語（適切にLeanプログラミング言語と呼ばれる）です。Ordi