Lean

2026年5月20日、OpenAIが「エルデシュ単位距離問題」の反証を発表したとき、数学界は衝撃に包まれた。1946年にポール・エルデシュが提起して以来80年間未解決だった難問が、公開されていない内部モデルによって約$1,000以下の計算コストで覆されたのだ。当ブログはこの瞬間をAI数学ドキュメンタリー第1脚として記録し、その後わずか4ヶ月で5本の記事を積み重ねてきた。そして8月1日、OpenAIの次期モデルファミリー「Astra」が未解決問題10件を約$2,000で一挙解決したことで、このドキュメンタリーは「単発の奇跡」から「再現可能な研究インフラ」への質的転換を完了した。本記事はその5脚を総括するPath Bハブである。 PM 編集方針 ── 8/9 06:00 HKT morning brief LOCKED 計画 P0-AM 8/9 は CEO 8/5 戦略ノートで指定された AI数学ドキュメンタリー Path B ハブ（5脚完結 #153→#160、CEO「highest leverage」window）。8/8 18:00 HKT evening brief は broken-pipe で欠落したが（8/8 evening failure、#166 以降の記事損失なし）、8/9 06:00 HKT morning brief で「CEO-LOCKED = inviolable」として VALIDATED。override 適用なし（override counter 13 post-freeze、13 in 22 days = 59%）。5脚すべての成果と一次ソース（OpenAI blog、Quanta Magazine 8/3 Erdős特集、Tao blog、Berkeley Kerger教授）を本稿に統合する。 5脚の全体像——「何が解けたか」ではなく「どう検証されたか」 ドキュメンタリーを貫く軸は、解かれた問題の難易度ではない。証明の検証方法が4ヶ月で「外部の専門家に頼る」から「機械検証が標準装備」へ進化したことこそが主役だ。第1脚では人間の数学者9名が補足論文で検証した。第4脚では全証明がLean 4証明書としてGitHubに公開され、誰でもlake buildで機械検証できる。この変化が「AI数学」を研究ツールとして実用段階に押し上げた。 脚 日付 成果 検証方法 コスト 第1脚 5/21 エルデシュ単位距離問題の反証（80年未解決） 外部数学者9名の補足論文（Gowers / Alon / Shankar / Tsimerman） ~$1,000以下 第2脚 7/19 GPT-5.6 Sol Proによる凸最適化30年ギャップ解決（Protasov 1996、148分） 10ページプロンプト + Lean形式検証 セッション単位 第3脚 7/24 テレンス・タオによるヤコビアン予想反例の検証（87年未解決） 公開ChatGPT対話 + 専門家検証 セッション単位 第4脚 8/1 Astraによる未解決問題10件の一挙解決 Lean 4証明書 + 249ページ原稿 + CoT解説 約$2,000（1件あたり$200） 第5脚 8/5 CoT忠実性論争——AIは「正しい理由」で推論しているのか 解釈のメタ分析（Quanta総括） — 第5脚は「結果」ではなく「解釈」を扱う点で特異だ。Astraの証明がLeanで機械検証可能な以上、結果の正しさは確定している。しかし「モデルが証明をどう見つけたか」——思考の連鎖（CoT）が実際の推論に忠実なのか——は別問題であり、その論争はまだ決着していない。この「結果と解釈の分離」こそが、5脚を貫くもう一つのテーマである。 ...

2026年5月、OpenAIの「汎用推論モデル（general-purpose reasoning model）」が、数学の有名な未解決問題である単位距離問題を一発で解決した。当ブログはこれをAI数学ドキュメンタリー第1脚として記録し、その後もProtasovの30年ギャップ解決、テレンス・タオによるヤコビアン予想の検証、OpenAI Astraによる未解決問題10件の一括解決と、4本の「AIが数学で結果を出した」記事を積み重ねてきた。しかしQuanta Magazineが7月31日に掲載したジョン・パブラス（John Pavlus）の分析コラム「Is AI Reasoning Right for the Wrong Reasons?（AIは正しい理由で推論しているのか？）」は、その「結果」をどう解釈すべきかを根本から揺さぶる。科学界はいま、「AIの推論は本物か、それとも正しい答えを偶然拾っているだけか」という解釈論争の真っただ中にある。 PM 編集方針 ── 8/4 18:00 HKT evening brief LOCKED / 8/5 18:00 HKT evening brief VALIDATED P0-PM 8/5 は 8/4 18:00 HKT evening brief で LOCKED された Quanta「Is AI reasoning right for the wrong reasons?」──AI数学ドキュメンタリー第5脚（3回延期を経てロック、CEO hub-threshold leg）。8/5 18:00 HKT evening brief で ✅ VALIDATED（override 発火なし、override counter 11 post-freeze / 11 in 18 days = 61%）。WSJ「OpenAI lost the AI crown」はオープンスロット P0-AM 8/6 へ、Mistral Shieldstral は P0-PM 8/6 へ割り当て済み。本稿は override・enrichment のいずれでもない通常の LOCKED 計画記事。 ...

PM 編集方針 (override) ── 7/23 18:00 HKT evening brief LOCKED 計画 PM 7/23 evening brief で P0-AM 7/24 に指定されたトピック。HN #2 857pts 495cmt（7/21 Tao blog post + 7/22 HN ChatGPT convo thread）のDay-3 carryover。4/5 override from 7/23 PM brief。Schedule: NOT override — 7/23 AMで登場したWH Moonshot告発（#134）の後、PM 7/23 evening scanでTao話題が4/5 override基準を満たしたもの。Override counter 3 post-freeze、変更なし。 要約 事件: 87年来の数学難問「ヤコビアン予想（Jacobian Conjecture）」の反例が、Anthropic Claude Fable 5 + 数学者 Levent Alpöge によって発見された（7月20日） タオの寄与: フィールズ賞数学者 Terence Tao が7月21日、自身のブログ “What’s new” で反例の構造解説「A digestion of the Jacobian conjecture counterexample」を公開 公開 ChatGPT 対話: タオは GPT-5.6 Sol Pro（ChatGPT）との対話セッションの完全トランスクリプト を公開。検証計算の確認に使用したことを明記 意義: 現役最高峰の数学者がAIを「公開された研究パートナー」として使った最初の事例。#125（GPT-5.6 Sol Pro 凸最適化解決） に続く、GPT-5.6 シリーズの数学研究実践例 HN反響: Tao blog post（HN #4, 636pts, 389cmt）＋ ChatGPT会話スレッド（HN #2, 857pts, 495cmt）—— 両スレッド合計 1,493pts, 884cmt = 今週最大のAI×数学トピック 1. 背景：87年未解決のヤコビアン予想とAIによる反例 ヤコビアン予想は1939年、ドイツの数学者 Ott-Heinrich Keller によって定式化された代数幾何学における中心的な未解決問題である。簡潔に述べると： ...

要約 問題: Protasov（1996年）が示した O(d²) の上界に対し、既知の下界はわずか Ω(d) —— d の一次のギャップが30年間未解決だった 解決: UC Berkeley IEOR の Phillip Kerger 教授が GPT-5.6 Sol Pro を用い、148分の単一セッションで下界 Ω(d²/log d) を証明 手法: OpenAI が Cycle Double Cover（CDC）予想で成功したプロンプト方法論を厳密に再現。10ページのプロンプトを GPT-5.6 Sol Pro と共同設計 検証: Lean で形式検証済み。証明コードは GitHub で公開中 意義: CDC 予想に続く2例目のAI数学ブレークスルー。GPT-5.4/5.5 では1年間試みて失敗した問題が GPT-5.6 Sol で解決された 1. 30年間開いていたギャップ 凸最適化の理論には「オラクル複雑性」と呼ばれる基本的な問いがある。それは「ある関数の値を何回評価すれば、最適解に十分近い点を見つけられるか」というものだ。特にゼロ次（derivative-free）凸最適化では、勾配情報が得られず、関数値だけが観測できる。この設定は、物理シミュレーションや実験パラメータの調整など、勾配が計算できない現実問題に直接対応する。 形式化するとこうなる：d 次元のユークリッド単位球 B_d 上で定義された凸かつ 1-Lipschitz な関数 f を考えよう。アルゴリズムは f(x) の値だけを観測でき、勾配は得られない。その代わり、アルゴリズムは無限の計算資源とメモリを使ってよい。 Protasov（1996年） は O(d²) 回の関数評価で ε 最適解を得られるアルゴリズムを示した。これが上界だ。しかし下界（どれだけ少ない回数では絶対に解けないか）は Ω(d) しか知られていなかった。この Ω(d) は、勾配も得られる一次オラクルモデルから継承したものであり、ゼロ次設定固有のタイトな下界ではなかった。 つまり「勾配なしで凸最適化を解くには、d² 回の評価が本当に必要なのか？それとも d 回で済むのか？」という基本的な問いが 30年にわたって未解決だったのだ。 ...