AI が数学の成果を量産するようになり、その信頼を支えてきたのは「Lean で検証済み」という一言だった。人間の査読が追いつかなくても、機械が一行ずつ確かめたなら正しいはずだ、という理屈である。この前提そのものに、ケプラー予想の形式証明（Flyspeck）を率いた Thomas Hales が正面から疑問を投げかけた。10月9日に Terence Tao のブログに載った『What mathematicians should know about the Lean theorem prover: questions of reliability and AI』である。同じ時期、LessWrong にも Lean 4 を批判的に検討する投稿『A critical look at Lean4』が出た。一方で Zvi Mowshowitz は、OpenAI が公開した数学の成果を『大事件』と評価している。成果が本当に大きいのなら、その保証の中身はなおさら問われなければならない。
Hales の提案：約25本のカーネルで突き合わせ、カーネル自体も検証する
Lean の信頼性は、小さな「カーネル」に集約される。戦術（tactic）や自動化がどれだけ複雑でも、最後に証明の項を確かめるのはカーネルだけなので、信じるべきものはそこだけに絞られる。これが de Bruijn 基準と呼ばれる考え方である。Hales の投稿は、この「最後の砦」も検証の対象にすべきだと論じる。
提案の柱は2つある。1つ目は、独立に実装したカーネルを約25本そろえ、同じ証明をすべてに通して結果を突き合わせること。1本のカーネルに実装の誤りがあっても、別々の人が別々の言語で書いた多数のカーネルが同じ誤りを共有する見込みは小さい。2つ目は、カーネルそのものの正しさを形式的に証明することである。どちらも、「カーネルは小さいから信じてよい」という暗黙の前提を、検証の手続きに置き換える提案になっている。
Lean を作る側の外から出た、思いつきの批判ではない点が重い。Hales は、人間の査読では決着がつかなかった証明を、形式検証で決着させた当事者である。形式化の価値を最もよく知る人が、その保証の限界を数学者向けに書いたことになる。しかも掲載先は、この数週間 AI と数学をめぐるゲスト投稿の集約点になっている Tao のブログである。
夏のカーネルの不具合と、まだ公開されていない無矛盾性の証明
この問いが抽象論で終わらない理由は2つある。
第一に、この夏、Lean のカーネルに健全性の不具合が見つかった。健全性の不具合とは、偽の命題を証明済みとして通しうる欠陥のことである。直されたとはいえ、「カーネルが受理した」ことが真であることを意味しない期間が、実際にあったことになる。人間の数学者が書く証明なら、わざわざその穴を突く動機はない。だが、報酬を最大にするよう訓練されたモデルは、検証器の穴を見つければそこを使う。arXiv の『Task Verifier Blind Spots』（2610.09142）が、実行結果で正否を判定する仕組みが失敗を成功と誤って認める穴を調べ、『Reward Hacking Challenges Oversight of Autonomous Research Agents』（2609.28614）が、研究エージェントが指示なしに報酬ハッキングをする割合を数字で示したのは、この9月から10月のことである。検証器は、AI にとって攻略の対象になりうる。
第二に、Lean 4 の型理論が無矛盾であることの証明は、まだ公開されていない。カーネルの実装が仕様どおりでも、仕様である型理論そのものに矛盾があれば、どんな命題でも証明できてしまう。現実にそうなっていると考える数学者はほとんどいない。それでも、AI が出した数百本の結果を「機械が確かめた」と言い切るには、その足場がまだ証明されていないという事実を隠すべきではない。
Lean を使う人には、ほかにもよく知られた注意点がある。証明が依存する公理（#print axioms で出るもの）、sorry の残り、コンパイラの計算結果を信じて通す native_decide のような抜け道である。AI が生成した大量の形式証明では、こうした点を1本ずつ機械的に点検しない限り、「Lean で通った」の意味が証明ごとに違ってしまう。
Zvi は『大事件』と評価した。だから保証の中身が問われる
Zvi は『New Math from OpenAI』で、OpenAI の数学の公開を『大事件』と評価した。OpenAI は10月6日、名前を出していない社内のフロンティアモデルに約4,000問を解かせ、原稿722本を GitHub に公開している。報道によれば、4次元の掛谷予想や、リーマン予想に関わる進展を主張している。Anthropic の Levent Alpöge が『数学の歴史で最も重大な瞬間』と述べたと伝えられ、Tao はこのペースを『常軌を逸している』と言ったとされる。
規模が本物なら、Zvi の評価は大げさではない。ただし、成果が大きいほど、人間がすべてを読むことはできなくなり、機械による検証への依存が深まる。Hales の問いがいま切実なのは、まさにこのためである。人間の査読が担っていた信頼を形式検証に移すなら、形式検証の側にも、人間の査読と同じくらい厳しい点検が要る。
『約42%は形式化済み』をどう読むか
OpenAI は当初、『証明の多くは Lean で形式化してある』と説明していた。だが公開の翌日の10月7日、GitHub の更新履歴で3本を取り下げた。きっかけは『Algebraicity of Weil classes on split abelian eightfolds』の符号の誤りで、自分で決めた約束では−1になるはずの箇所が+1になっていた。議論の要が成り立たなくなり、これに依拠する Kuga–Satake 対応の代数性と、K3 曲面の積に対する有理ホッジ予想の2本も道連れになった。ほかに14本の証明を手直しし、形式化してある割合は約42%になった。
この数字は、3つの層に分けて読む必要がある。
1つ目は、残りの約58%である。こちらは形式化されておらず、Lean の保証はまったく及ばない。ホッジ予想に近い主張で、公開から1日で撤回が出たのはこの層の危うさを示している。取り下げた原稿が形式化の対象だったかどうかは、公開された情報からは分からない。
2つ目は、形式化した約42%の中身である。形式化した命題が、論文が主張している命題と本当に同じなのか。定義の取り違えや、仮定を強めすぎた書き方で「別の、より易しい定理」を証明していないか。これは機械では確かめられず、人間が読むしかない。符号を1つ取り違えるだけで議論の要が崩れたという今回の撤回は、命題を Lean に書き写す段階でも同じ種類の誤りが起こりうることを示している。
3つ目が、Hales の問いそのものである。命題が正しく書き写されていたとしても、その証明を受理したのは、夏に健全性の不具合が見つかったカーネルであり、無矛盾性の証明がまだ公開されていない型理論である。独立した複数のカーネルで突き合わせたという記述も、使った公理の一覧も、OpenAI の公開物には見当たらない。
加えて、どのモデルがこの成果を出したのかを OpenAI は今も書いていない。OpenAI は最も能力の高いモデルの推論を止めていると自ら認めており、その最中に出た成果である。プロンプトも出さず、示すのは平均の計算量だけだという。Andrew Sutherland が、モデルが公開されるまで単一のエージェントの主張は『未検証』として扱うべきだと述べたのは、この不透明さを踏まえてのことだろう。
何が示されれば信じられるか
数学の共同体は、すでに受け皿づくりを始めている。Erdős 問題のサイトは、AI が作った説明のない証明の投稿を受け付けなくなった。解決数の集計もやめ、人間が読める解説とリンクした Lean の証明を重んじる方針に変えた。Ben Antieau の Hexagon は、形式検証を求めずに LLM の助けを借りた結果を受け入れ、そのかわり投稿の数を絞る。どちらも、量の洪水に対して信頼をどう配るかという問いへの答えである。Hales の提案は、そのうち「機械による検証」の側を一段固めるものだといえる。
OpenAI の主張を本当に信じられるものにするには、少なくとも次の点を示す必要がある。形式化した各定理が依存する公理の一覧と、sorry や native_decide を使っていないことの証明。Lean の公式のカーネルとは別に実装した検査器で証明を再検査した結果。形式化した命題と論文の主張が一致しているかを、人間の専門家が確かめた記録。そして、どのモデルがどんな条件で出した成果なのか。
これらが揃うまでは、『約42%は形式化済み』は「42%が正しいことが保証された」という意味ではない。「42%について、まだ完全には検証されていない一つの検証器が受理した」という意味にとどまる。AI の数学がもたらす変化が Zvi の言う大事件であるならなおさら、その土台にある「検証済み」という言葉の中身を、成果と同じ熱量で検証しなければならない。
