OpenAIの内部最新推論モデルが、10の驚異的な数学的進展を一斉に発表しました。
これには：
- 非ソフィック群（Non-sofic groups）の存在が初めて証明された；
- 新しい回路下界が提示された；
- 最近のベクトル問題（Closest Vector Problem、CVP）の難易度限界を突破した；
- および双人量子ゲームの並列反復指数減衰定理（Quantum parallel repetition）。
コロンビア大学の准教授であるHenry Yuenが最も気にするのは最後の一つである——
2016年、Yuenはこの問題で大きな進展を遂げたが、完全には解決しなかった。10年間、彼は度重なる失敗を経験し、 even 1か月前にもChatGPT 5.5を使って最終的な証明に挑んだが、得られたものはわずかだった。
そしてAIは彼の肩に乗って、軽く一脚でボールをゴールに決めた。
証明は正しいが、人類は理解しなかった
数日前、Chen LijieはHenry Yuenと他の数人に論文の下書きを送った。
当時、生活が忙しく、彼は深く研究する余裕がなかった。今、論文が公開された。彼は言いたいことがあり、我慢できない。
量子並列繰り返し定理（Quantum parallel repetition theorem）は、Henry Yuenが大学院生時代に数年にわたって心血を注いで研究した分野であり、彼が最も誇る成果である。
ヘンリー・ユンは、現在コロンビア大学のSrivaniファミリー計算機科学准教授です。
彼は、カフェで過ごした午後、オフィスで過ごした深夜、そして休むべきだった無数の週末を、ラン・ラズの古典的並列繰り返し定理を繰り返し分解し、研究していたことを覚えている。
彼はこの定理の量子版を解決しようと、夜も眠れず、寝返りを打った。彼は膨大な数学的ツールを駆使し、最終的に多項式減衰を証明した。
https://arxiv.org/pdf/1604.04340
さらに重要なのは、彼がその中で自信を築き、ようやく自分の実力を認識し、自分が確かに（少なくとも一部）他の人も気にする問題を解決できることを証明したことです。
彼は、Leanの形式化証明がすでに存在するため、OpenAIのこの証明は正しいはずだと信じている。しかし、この新しい証明を理解するには、ヘンリー・ユンにとってまだ時間がかかる。
新しい証明は確かに彼の以前の証明の続きから始まっているが、AIは彼の従来の証明戦略の制約を乗り越え、演算子理論や関数解析の分野で研究者たちがすでに掌握している可能性のあるいくつかの手法を使用した。
興奮の一方で、Yuenの最初の感想は失望だった、論文の書き方に対する失望だった。
彼はこの証明書がAIらしさに満ちていると言った：長々とした導入が繰り返され、肝心の部分はまるでマジックのように、読む者を混乱させる。
OpenAIの証明は読むと興味深いが、やや頭を悩ませる。
それはまず問題をまっすぐ机の上に置き、その後、突如として「予解式を使って正しいpurificationを見つける」という方向に飛び移り、その間にほとんど論理的な段階を残さない。
次に、一連のやや珍しい行列エントロピー計算が行われ、複雑な計算を経て、この道は可行であると結論づけられます。
しかし、最も重要な一歩、その直感がどこから来るのかは、述べられていない。
そして、最も精妙で、創造力を最も問う那一筆——Uhlmann変換を用いた演算子空間の膨張のテクニックは、本来、この証明の最も感動的なクライマックスであるべきだったが、AIはそれを泥砂のように見捨て、予告もなく、説明もなく、第4節に放り投げた。
正しい証明だが、最も重要な考えを隠している。
彼はOpenAIにもう少しプロンプトを工夫して、この原稿をしっかり整理してほしいと思っています。
さらに心に刺さるのは、第二の層：Leanの検証が通ったからといって、理解したわけではないということだ。
機械はすべての推論ステップを完璧に保証できますが、「この手法がなぜ有効なのか」「それはより広い理論の地図上で何を意味するのか」「どこにさらに応用できるのか」といった質問には、Leanは一つも答えられません。
ユエンは、この証明を今でも消化していると率直に語った。
答えは眼前にありながら、彼はAIが口にしなかった直感を、素人の論文を読むように一行ずつ再構成しようとしている。
はい、確かに形式的な証明は存在します。しかし、それは形式化に過ぎず、私が理解したことを意味しません。本当の理解を得るには、時間がかかるしかないでしょう。
確かに、AIは人間の理解の境界を広げましたが、その後何が残るのでしょうか？研究の楽しさや意味はどこにありますか？AIが彼が夢中になっていた難題をすべて解決してしまったら、彼には何が残るのでしょうか？
質問が次々と寄せられた。しかし、彼はますます確信した：数学者の今後の日々は忙しくなるだろう。これらの思想の巨獣を制御し、それらの専門用語を一般の人にもわかる言葉に翻訳しなければならないからだ。
AIが「反証」した百年の数学予想が偽りと判明！Leanも安全な箱ではない
先週、ラマナ・クマールは、300行のLeanを用いて、最も有名な数学の未解決問題である「コラッツ予想」を反証した。
彼が尋ねた質問は非常に単純です：正の整数を与えられ、次の2つのルールに従って繰り返し操作します——偶数なら2で割り、奇数なら3を掛けて1を足す——そのとき、どの数から始めても最終的に1に到達するのでしょうか？
計算できます：
この仮説は、どの正の整数から始めても、最終的に4→2→1の循環に陥るというものです。
この問題は、数学者ローター・コラッツが1937年に提起して以来、証明されることも、反例が見つかることもありません。
数学者ポール・エルデシュはこれを「数学はこのような問題にまだ対応する準備ができていない」と呼び、アメリカ国立アカデミー院士で数学者のジェフリー・ラガリアスは「これは異常に難しい問題であり、現代数学の範囲をはるかに超えている」と考えている。
もし反証された場合、それは数学界にとって画期的なニュースとなる无疑である。
残念ながら、3日後に、この形式的なLean証明は、実際にはLeanカーネルの下位レベルの脆弱性を悪用していたため、無効と判定されました。
OpenAIのDaniel Selsamが、サイバーセキュリティに特化したAIを用いて、Lean FROのカーネル監査を支援しました。
結果、彼らはLeanカーネル内に複数の脆弱性を発見しました！
ほぼ同時に、ラトガース大学の数学教授でLean特別研究組織のアドバイザーであるアレックス・コントロロビッチが投稿し、Leanを万能の検証者とみなすべきでないと注意した。
他の直指する弱点——意味的整列（Semantic Alignment）。
Leanのカーネルが完璧であっても、Leanはコードのコンパイルのみを担当する。あなたがコードに記述した「定義」と、人間が自然言語で持つ「直感的な意図」が同じものであることを誰が保証するのか？
Leanが確認できるのはたった一つのことだけだ：コードはコンパイルを通って、形式論理的に矛盾していないということ。しかし、それはもっと重大な問題——この形式的記述が、本当に証明したい定理に対応しているのか——を検証しない。
定理は正しいが、問題を間違えて書き写した。Leanは依然としてグリーンライトを出した。
しかし、このアラインメントの問題は、コンピューターだけでは解決できません。
ICM 2026の講演で、コントロロビッチは指摘した：形式化数学の最大の盲点は「導出を正しく行うこと」ではなく、「正しい言葉で述べること」である。最終的なチェックは、依然として人間の専門家が行う必要がある。
当時、Liquid Tensor Experimentが神格化されたのは、研究者が各数学的定義に対して近乎偏執的な手動での検証を行ったからである。
二人の教授の言葉を合わせて見ると、同じ事実を示している：AIは証明できるし、機械は検証できるが、理解し管理するのは依然として人間の仕事である。
最後に、AI推論モデルに関する噂があります：
参考資料：
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
本文は微信公衆アカウント「新智元」より、著者：ASI启示録；編集：ダビッド