ハクソク

世界を動かす技術を、日本語で。

数学者が知っておくべき「Lean定理証明器」について：信頼性とAI

2026年10月10日原文(terrytao.wordpress.com)

概要

  • 数学の一貫性と信頼性が文明と科学を支える基盤であることを強調
  • 数学の形式化と証明支援システム（Leanなど）の発展経緯を解説
  • AIによる自動形式化（autoformalization）の現状と急速な進展を紹介
  • Leanの型理論、設計思想、信頼性の検証手法を説明
  • 2026年夏に発生した「サウンドネスバグ」の事例とその意義を考察

数学の価値と形式化の重要性

  • 数学の一貫性 と 信頼性 が科学や社会の基盤

  • 形式的証明： 数学の基礎 と 論理規則 レベルで完全に検証された証明

  • 主要な形式化プロジェクト例： 四色定理、 Feit-Thompson定理、 Kepler予想、 Fermatの最終定理 など

  • 証明支援システム（proof assistant）： Automath、 HOL Light、 Isabelle、 Coq（現Rocq）、 Metamath、 Mizar、 Lean

  • Leanは 数理学者に最も人気 のある証明支援システム

    • 2013年に Leo de Moura がMicrosoft在籍中に開発
    • オープンソース化 により普及が加速
    • 2017年、 mathlib ライブラリが誕生し、現在は 約30万定理、 10万定義、 250万行超のコード、 700人以上の貢献者

自動形式化（Autoformalization）の現状

  • 以前は 人手で論文証明を形式化 していた（Kepler予想形式化は 20人年、 50万行）

  • AIによる自動形式化 が2026年に実用段階へ

  • 主要なマイルストーン

    • 2025年9月： Math Inc. が素数定理の準自動形式化
    • 2026年1月： J. Urban がトポロジー教科書の大部分を2週間で自動形式化
    • 2026年3月： 24次元球充填問題 の自動形式化（ Math Inc.、50万行→20万行に圧縮）
    • 2026年5月： Meta/Facebook Research が26冊の教科書をATLASプロジェクトで自動形式化
    • 2026年9月： Anthropic がFermatの最終定理を 11日間で1300万行 で自動形式化
    • 2026年9月： OpenAI がNavier-Stokes強制ブローアップ定理をLeanで自動形式化

  • MAP（Mathematics Autoformalization Project） が「既知の全数学の形式化」を目指し始動

Leanの信頼性と型理論

  • Leanは 型理論（type theory） に基づく証明支援システム
    • 特に CIC（帰納的構成の計算論） を採用
  • 型理論 と 集合論 の互換性
    • Werner (1997) 論文で、ZFC集合論とCIC型理論の相互変換が可能と示される
  • 型理論の直感的説明
    • 型＝交わらない集合 と見なせる
    • 例： 2 の型は自然数型、 e の型は実数型、明示的な型変換も可能

Leanの設計と検証プロセス

  • Leanは 汎用プログラミング言語 と 数学言語 を統合
    • プログラムと定理証明を 同一言語 で記述可能
    • 証明スクリプトは elaboration（精緻化） を経て Leanカーネル が検証
  • Leanカーネル は数千行のC++で実装、 極めて重要な信頼性要素
  • mathlib ライブラリ全体（250万行）もカーネルで検証
  • Leanでの証明は カーネル検証後 に 人による監査 も必要
    • 定義や定理が 本来の意味と一致 しているかを確認
    • Leanの比較ツール で定義の正当性や不正な公理の混入もチェック

サウンドネスバグとその意義

  • サウンドネスバグ（soundness bug） ：カーネルのバグで「偽」証明が成立してしまう深刻な問題
  • 2003年、 HOL Light で著者がサウンドネスバグを発見
  • Lean 4 （2023年リリース）でもリリース前に2件、2025年に1件のサウンドネスバグが修正
  • 2026年夏、「サウンドネスバグの夏」 として複数のバグがLeanで発見
    • Collatz予想の不正な反証やKepler予想の偽証明も発生
    • 全て 迅速に修正 され、mathlibも再検証済み
  • サウンドネスバグの発見は 信頼性向上の好材料
    • セキュリティ研究者とAIによる積極的な検証活動
    • 例： Ramana Kumar や Dan Selsam などが主要なバグ発見者

数学形式化の未来展望

  • 自動形式化の普及 により、今後数学の証明や定理の形式化は 容易かつ日常的 になる見込み
  • Leanをはじめとする証明支援システムの 信頼性向上 と AI活用 が鍵
  • 「既知の全数学の形式化」 という壮大な目標に向けて、研究と開発が加速

Hackerたちの意見

自動形式化は2026年に実用的な現実になった。うーん、多分。ここ一週間、論文をleanに翻訳してたんだけど、形式化された結果と論文の相関関係はめっちゃ悪い。サイクルは「論文に挑戦してみる、ちょっと難しい、別のことを証明する、成功を宣言する」って感じ。手作業でやるよりは速いけど、論文を入力してleanを出力するからって、二つの間に対応関係があるわけじゃないんだよね。

└

別のことを証明する それって「少し違う道を使って最終的な結果を証明する」ってことかな？よく分からないけど。

└

独立したレビュアーが論文のテキストを生成されたLean形式化と比較したとき、AIが壁にぶつかるたびに、静かに文を変えていたことがわかった。例えば、4階の導関数を5階に引き上げたり、符号インデックス（+1対-1）を変えたりして、証明チェッカーがコードを受け入れるようにしていた。Leanカーネルはコンパイルされたコードが論理的に一貫していることを確認する役割を果たしたけど、そのコードは英語の論文が主張していることを証明していなかったんだ。

└

80年代から90年代の論文を何十本かLeanで形式化したけど、著者の誤字や直球のエラー、時には間違った表現がかなり怖いくらい多かったよ。解決の道筋は著者が示したものとは違うかもしれないけど、少なくとも手作業では見つけにくい問題を簡単に見つけられるのは良いところだね。

leanカーネルでまたサウンドネスバグを見ることはあるのかな？ソフトウェア開発者にとっては、そんな質問は狂ってるように思える。過去にもバグはあったし、これからも出てくるだろう。もしバグが見つかったら、それはAIのlean証明にとって何を意味するんだろう？信頼できるのかな？結局、これって信頼の問題なんだよね。人間の検証はコミュニティや評判、そして人間の労力によって高い信頼性がある。人間は時々数学の結果について嘘をつくけど、これは稀だから。間違いを犯すこともあるけど、その間違いはコミュニティによって発見される。LLMは評判なんて気にしないし、よく幻覚を見たり捏造したりする。制約の中では、文字通りルールを破ろうとするから、ルールに基づいた知識には大きな災害になる。だから、証明チェッカーに頼る必要があるんだ。でも、証明チェッカーはどれだけ信頼できるのか？バグはあるのか？そして、その基礎理論自体は逆説や未知のもの、利用される可能性のある数学的な「バグ」から自由なのか？他の数学者を騙そうとする人間の数学者を想像してみて。彼らのブレークスルーを、たとえ検証者がいても信じられるだろうか？こういう特性があるから、最終的には人間がバックストップにならなきゃいけないし、コミュニティや労力に基づいた人間の信頼システムに根ざしているべきなんだ。今のところ、人々はツールを過信しすぎてる。予測：人間がAIツールを使ってNavier-Stokesの証明に疑問を投げかけるバグを見つけるだろう。

└

問題は、証明チェッカーはどれだけ信頼できるのか？バグはあるのか？そして、その基礎理論自体は逆説や未知のもの、利用される可能性のある数学的な「バグ」から自由なのか？他の数学者を騙そうとする人間の数学者を想像してみて。彼らのブレークスルーを、たとえ検証者がいても信じられるだろうか？ --- > 検証されたLeanカーネルの秋 この記事のこのセクション（およびその直後のセクション）を読んだ？あなたの考えに部分的に触れてるみたいだよ。コメントしてみたらどうかな？

└

未発見のサウンドネスバグが存在しても、Leanで証明されたすべてが不正というわけではない。証明がそのバグを利用しなければならないから。人々は、地殻の状況が健全でないかもしれないのに、健全な基盤の上に家を建てるんだ。 > こういう特性があるから、最終的には人間がバックストップにならなきゃいけない... 投稿では、Leanの基礎となるメタ理論の作業がまだ終わっていないことが明確に述べられていて、さらなる作業が必要だと言ってる。コンピュータ形式検証が数学そのものの信頼性に達することが不可能だとは思えないよ。

└

コーヒー牛乳プロジェクトに興味があるかもしれないね。Leanの定理証明器の一部で、Leanのmathlibの全内容を証明するのに十分な部分が、一貫性があることが証明されたんだ。

└

確かに、今のLeanカーネルでもまたサウンドネスバグが出る可能性は高いね。他の証明支援ツールでも同じだと思う。ただ、証明の正確性に関しては、個人的にはそれほど心配してないかな。欠陥のある証明を取り込もうとする側と、それを防ぐためにカーネルを強化しようとする側、どちらもAIを味方にしてるからね。AIがもっと進化して賢くなれば、両方の側で使えるようになる。防御側の方が楽な仕事だと思うけど。ナビエ-ストークスの証明についてはよく分からないけど、一般的には多くの有名な定理が間違っているとは考えにくいよ。もっと心配なのは、テレンス・タオが話しているような問題だね。つまり、証明された定理は本当に私たちが興味を持っている定理なのか？分野の基本的な定義は正しく述べられているのか？そういう質問だよ。それに、カーネルではない証明支援ツールの部分もまだあって、それが悪用される可能性もある。例えば、きれいなプリンターやパーサーを使って、実際とは違うように見せることができるんだ。ある公理を導入しながら、それが追加されたことをタイポグラフィ的に隠すこともね。確か、何年か前にCoq（今はRocq）の定理証明器でその例を見たことがあるんだけど、具体的にどうだったかは忘れちゃった。

└

openai-wilesの撤回は教訓的だね。まず第一に、openaiは彼らが証明した定理を形式化していない。おそらく、Leanのmathlibをかなりアップグレードしないといけなかったからだろうね（または多くの既存の定理を公理としてシムする必要があったけど、OpenAIはそれを選ばなかった）。面白いことに、よく知られた定理をシムすると、証明のエラーは明らかにならない（要するに、不変量を追跡するための競合する慣習があって、定理が互換性がないんだ）ってことは、分野で働いてないと気づかないかもね？ 定理チェッカーは、数学の根本にまで行かないと慣習の互換性をチェックできないんだ。openaiによる撤回された証明の形式化に興味があるなら（ドキュメントのLLM用語にはごめんだけど、それがポイントだから、LLMはXYZできるのか）：https://github.com/ityonemo/openai-wiles

└

古いものは新しくなる。 https://people.cs.umass.edu/~emery/classes/cmpsci691st/readi...

└

人間はしばしば間違えるし、時には壊滅的に間違えることもある。正確であるインセンティブがあってもね。誰もが人間は完璧じゃないって知ってるけど、あなたみたいな人は、その影響があまりにも不快になるとそれが真実じゃないふりをするよね。

Hacker Newsで議論の続きを見る