Lean 4とは — AIが数学を証明する2026年、注目の定理証明支援系と日本語で学べるLean-ja

Lean 4は、マイクロソフトリサーチ発祥で現在は非営利団体Lean FROが開発を主導する、純粋関数型プログラミング言語かつ証明支援系（Proof Assistant）です。最大の特徴は「依存型」と呼ばれる表現力の高い型システムを備えている点で、これによりプログラムが書いたアルゴリズムの通りに動作することを型レベルで「証明」できます。証明を書いてコンパイルが通れば、その証明は正しいと確信できるという仕組みです。証明の一部自動化や、強すぎる仮定を自動検出する支援機能も備えており、大学学部レベルの数学のかなりの部分がmathlib4という共同ライブラリを通じてすでにLean上で形式化されています。ブラウザから直接試せる「Lean 4 Web」も用意されており、環境構築なしに動作を体験できます。2026年に入り、このLean 4がAIによる数学研究の基盤技術として急速に注目を集めています。

大規模言語モデル（LLM）は、もっともらしく聞こえるが実際には誤っている回答、いわゆる「ハルシネーション」を生成することがあります。数学の証明のように一つの論理的な飛躍も許されない領域では、この弱点が致命的になります。ここでLean 4が果たす役割が、AIが生成した証明の候補を機械的に検証する「審判」です。Leanでは証明がコンパイルを通れば、その正しさが数学的に保証されます。つまり、AIが大量の証明候補を生成し、Leanがそれを厳密に検証するという分業体制が成立するわけです。AIの発想力・探索力と、Leanの厳密な検証能力を組み合わせることで、人間の専門家だけでは時間がかかりすぎる証明にも取り組めるようになった、というのが2026年に起きている変化の本質です。

2026年に入ってから、AIとLeanを組み合わせた成果が相次いで報告されています。主なものを整理すると次の通りです。

AlphaProofはAlphaZero系の強化学習エージェントを源流に持ち、2024年のIMOで銀メダル相当の成績を収めた実績があります。そこからさらに発展したAlphaProof Nexusが、今回エルデシュの未解決問題という未踏領域に踏み込んだ点が注目されています。

Lean 4を実際に体験する最も簡単な方法は、ブラウザで動く「Lean 4 Web」を開くことです。インストール不要で、簡単な関数の定義や証明をその場で書いて実行結果を確認できます。Lean 4の型システムは「依存型」と呼ばれ、値によって型そのものが変化する表現力を持ちます。たとえば「要素数がちょうど3個であるリスト」のように、リストの長さという値の情報を型に組み込むことができ、コンパイラがその制約を静的にチェックしてくれます。数学の証明で言えば、「この命題が真である」ということ自体を型として表現し、その型に対応する値（証明項）を実際に構築できればコンパイルが通り、命題の正しさが保証される、という仕組みです。

- Lean 4 Web — ブラウザで環境構築なしに試せる公式のオンライン実行環境
- mathlib4 — 大学学部レベルの数学のかなりの部分を形式化した共同ライブラリ
- lean-ja — 日本語でLeanを学べるコミュニティサイト（後述）

Lean 4の情報は英語が中心ですが、日本語での学習リソースを提供しているのがlean-jaというコミュニティサイトです。Leanの基本的な考え方から実践的な使い方まで、日本語の解説を通じて学ぶことができます。英語のドキュメントに抵抗がある場合の入り口として活用できます。

Leanは数学の証明のための専用ツールですが、その根底にある「AIが大量に生成し、機械が厳密に検証する」という考え方は、数学の世界に閉じたものではありません。AIが生成したコードをどう検証し、安全に運用するかという課題は、ソフトウェア開発の現場でも同様に重要度を増しています。たとえばOpenAI Codex Securityの検証フェーズで紹介されているような、AIが生成した成果物を機械的にチェックする仕組みも、根本にある発想はLeanと地続きです。AIの生成能力を無条件に信頼するのではなく、検証のレイヤーをどう設計するかが、今後のAI活用における共通の論点になっていくと考えられます。

Lean 4は依存型を備えた証明支援系であり、証明の正しさをコンパイラが機械的に保証できる点が最大の特徴です。2026年に入り、AlphaProof Nexusによるエルデシュ未解決問題の証明、Gaussによる強い素数定理の形式化、IMO 2025での金メダル相当の成績など、AIとLeanを組み合わせた成果が相次いで報告されています。AIが証明候補を大量に生成し、Leanがそれを厳密に検証するという構図は、数学の世界にとどまらず、AIが生成した成果物をどう検証するかという、より広いテーマにもつながっています。日本語で学びたい場合はlean-jaが良い入り口になります。