2026 年 10 月 6 日（UTC）、OpenAI が GitHub に openai/math というリポジトリを公開しました。
中身は、まだ公開されていない社内モデルが出した数学の原稿で、2026 年 10 月 12 日時点の README では 719 本が並んでいます。
主な結果のおよそ 4 割には、Lean という言語で書いた証明が付いています。
openai/math（GitHub）
Lean の名前は、この秋の AI のニュースで何度も出てきました。
Lean の公式サイトの年表にも、2026 年 9 月に Anthropic がフェルマーの最終定理の Lean での形式化を発表したことや、OpenAI などがナビエ–ストークス方程式の問題で Lean で検証した結果を発表したことが並んでいます。
Lean が何を確かめてくれるのかが分かると、「AI が証明した」という発表のどこまでを機械が保証していて、どこから人の確認が要るのかを読み分けられます。
Leanとは
Lean は、オープンソースのプログラミング言語であり、数学の証明を書いて機械に確かめさせる「証明支援系」でもあります。
Lean（公式サイト）
公式の入門書『Theorem Proving in Lean 4』によると、Lean は 2013 年に Microsoft Research の Leonardo de Moura が始めたプロジェクトで、Apache 2.0 ライセンスで公開されています。
同じ入門書は、コンピューターが証明を助ける方法を 2 つに分けています。
- 自動定理証明: 証明を「見つける」ことに力を入れる。速くて強力だが、ツール自体のバグで誤った結果を出すことがある
- 対話型定理証明: 証明が正しいかを「確かめる」ことに力を入れる。すべての推論を基本の公理と規則までさかのぼって正当化させる
Lean はこの 2 つの橋渡しを目指していて、自動化の道具を使いながらも、最後は公理までさかのぼれる証明を組み立てます。
数学の定義や定理を集めたライブラリ Mathlib もあり、公式サイトでは 100 万行を超える規模と紹介されています。
Leanはどう確かめるか
Lean では、定理を「主張」と「証明」の組で書きます。
主張は「何が成り立つか」を Lean の言葉で書いたもので、証明はそれを導く手順です。
証明を最後に検査するのは、Lean の中心にある小さな検査器（カーネル）です。
公式サイトは、この最小限の信頼すべき部分（minimal trusted kernel）が証明の正しさを保証すると説明しています。
検査を通らない証明は受け付けられないので、証明の途中に飛躍や計算ミスがあれば機械が見つけます。
ただし、証明を書く途中で使う「穴」もあるので注意してください。
sorry と書くと、どんな主張でも証明したことにできます。
入門書の「Propositions and Proofs」の章は、これが証明の方法としては不健全で、使ったファイルには Lean が強い警告を出すと説明しています。
もう 1 つの抜け道が公理です。
公理は証明なしで正しいと認める前提で、#print axioms というコマンドで、ある定理が最終的にどの公理に頼っているかを一覧できます。
入門書の「Axioms and Computation」の章によると、Lean の標準ライブラリは propext・Quot.sound・Classical.choice といった公理を定めています。
AIの証明を受け取るComparatorの役割
AI が書いた証明を受け取る側には、もう 1 つ心配があります。
証明する側が主張の書き方をこっそり変えていたら、正しい証明が付いていても、確かめたいこととは別のことが証明されているかもしれません。
この心配に答えるのが、Lean の開発元 Lean FRO が作った Comparator という道具です。
leanprover/comparator（GitHub）
README によると、Comparator は AI の数学コンテスト AIMO で、LLM が書いた Lean の証明を信頼して採点できるようにする目的で作られました。
使い方は、確かめる側が「Challenge」というファイルに主張だけを書き、証明する側が「Solution」に同じ主張と証明を書いて渡す形です。
次は openai/math に入っている Challenge の 1 つで、証明の部分は sorry のままになっています。
-- openai/math の lean/ComparatorChallenges/QuasiRiemannHypothesis.lean（全文）
import Mathlib
namespace OAI
theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
{s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
sorry
end OAI読み方は「実部が 7/8 より大きい複素数 s では、リーマンのゼータ関数が 0 にならない」です。
原稿の目録では、この結果を quasi-Riemann hypothesis の解決と説明しています。
Comparator が通ったときに保証されるのは、次の 3 つです。
- Solution の定理が、Challenge と同じ主張を証明している
- 使った公理が、設定で許した公理（上の Challenge の設定では標準ライブラリの 3 つ）に収まっている
- Lean のカーネルが証明を受け付けた
2026 年 10 月 12 日時点の openai/math では、形式化の目録（formalization.yaml）に主な結果を形式化した論文が 173 本並び、主な結果 200 件のそれぞれに Comparator の設定ファイルが指定されています。
機械が保証しないこと
Comparator の README は、保証の前提も書いています。
いちばん大事なのは、Challenge のファイルとそれが読み込むライブラリを、確かめる側が自分で管理しているか信頼できることです。
ほかに、Lean のカーネルにバグがないことと、証明を検査するときのサンドボックスが破られないことも前提に入っています。
裏返すと、Challenge に書いた主張が、論文の言いたいことを正しく表しているかどうかは、機械は確かめません。
README には、主張の一部を空欄にして「Solution 側で埋めてよい」とする形の問題は、すり抜けられることがあるという例も載っています。
たとえば、リーマン予想が正しいかどうかを True か False で答えさせるつもりで、答えの欄を空けた問題を作ったとします。
答えの欄にリーマン予想そのものを書けば、「リーマン予想はリーマン予想と同値」という中身のない証明で通ってしまうのです。
そのため README は、この形の問題は必ず人などの別の検証者が確かめるように求めています。
AI が評価の抜け道を突く現象はリワードハッキングと呼ばれ、この例と同じ構図です。
形式化されている範囲にも注意が要ります。
openai/math の README は、すべての原稿に Lean の証明が付いているわけではなく、形式化されていない結果には問題が含まれうると明記しています。
さきほどのゼータ関数の結果の説明ページでも、論文の後半にある応用は形式化に含まれていないと書かれています。
確認の段階を書く目録の「review」欄は、unchecked（未確認）です。
目録の書式では、この欄に「agent-reviewed」「peer-reviewed」なども書けるので、今後どの段階まで確かめられたかはここで追えます。
発表を読むときの3つの問い
Lean 付きの発表は、機械で確かめた部分と、人が読むしかない部分が分かれています。
読むときは、次の 3 つを確かめると整理しやすくなります。
- どの主張が形式化されたか（原稿のすべてか、主な結果だけか）
- 形式化された主張の文を、誰が書いて誰が読んだか
- 形式化されていない部分は、どう扱われているか
openai/math の README によると、ほとんどの結果は同じ手順で作られ、1 つの結果に平均で ChatGPT Pro の約 3 時間分の思考の計算量が使われました。
モデルに出された問題は、約 4,000 問です。
推論に時間をかけるモデルの仕組みは、別の記事で説明しています。
Lean は数学だけでなくソフトウェアの検証にも使われていて、公式サイトでは AWS が認可ポリシー言語 Cedar の検証に Lean を使っている例が紹介されています。
AI が出した結論を、機械で検査できる形で受け取るという考え方は、テストを書いて AI のコードを確かめるのと同じ方向を向いています。
最後に
Lean は、主張と証明を書けば、証明が正しいかを小さなカーネルで確かめてくれる道具です。
Comparator を使えば、AI が書いた証明が、確かめる側の用意した主張と同じものを証明しているかまで機械で確かめられます。
一方で、主張の文が数学的な意味を正しく表しているかと、形式化されていない部分が正しいかは、人が読むしかありません。
「Lean で検証済み」という言葉を見たら、どの主張が、誰の書いた文で検証されたのかを確かめると、発表の重さを自分で測れます。
以上です。
コメントを残す