北京大学の数学者ドン・ビン率いるチームが開発したAIフレームワークが、2014年にアイオワ大学教授のダン・アンダーソンが提起した可換代数の未解決問題を解決した。
アンダーソンは2022年に死去している。AIは推論エージェント「Rethlas」と形式化エージェント「Archon」の2つで構成される。Rethlasは定理検索エンジン「Matlas」を活用して証明の候補を導き出し、Archonは「LeanSearch」を用いてその証明を定理証明器「Lean 4」向けのプロジェクトへと変換・形式化した。Lean 4のライブラリには数十万の定理と定義が収録されている。実行時間は80時間で、人間のオペレーターによる数学的判断は不要だった。研究論文はarXivに投稿されており、査読は未完了である。
From: Chinese AI cracks decade-old maths problem without human input
【編集部解説】
今回の研究が示すのは、単に「AIが難問を解いた」という事実ではありません。数学という営みそのものが、自動化の射程に入り始めたという、より根本的な転換点です。
まず、このニュースで最も誤解されやすい点を整理しておきましょう。「AIが数学の問題を解く」という報道は近年珍しくありません。しかし、大規模言語モデル（LLM）が生成する証明は「それらしく見えるだけ」のことが多く、数学的に正確かどうかは別問題です。今回の研究が一線を画すのは、証明を「生成」するだけでなく、「機械的に検証する」ところまでを人間なしに完結させた点です。
具体的には、推論エージェントRethlas が証明の候補を作り、それを形式化エージェントArchonがLean 4という証明支援言語に翻訳し、機械が読める形で正しさを保証します。Lean 4とは数学の定理を厳密なプログラムとして記述する言語であり、その証明はコンピューターが一行一行チェックできます。「なんとなく合ってそう」ではなく、「数学的に正しい」ことが保証された証明を、自律的に生成できたという点が本質的な意義です。
ポジティブな側面として最も大きいのは、数学研究の「生産性の壁」を突き崩す可能性です。未解決問題の探索や証明の形式検証といった、専門家でも数年を要しうる作業が、AIによって大幅に圧縮されるとすれば、数学・物理・暗号理論・材料科学など、証明に依拠するあらゆる分野の基礎研究が加速します。
一方でリスクも見落とせません。今回の論文はarXivへの投稿段階であり、まだ査読を経ていません。形式証明が出力されたとしても、前提となる問題の設定や証明の方針そのものが妥当かどうかは、依然として人間の数学的判断に依存する部分があります。また、AIが「解いた」問題が本当に意味のある問題であるかを評価する眼も、まだ人間が持ち続ける必要があります。
長期的な視点では、数学研究の役割分担が変わることが予想されます。ルーティンな証明の生成・検証はAIが担い、人間の数学者は「どの問いを立てるか」「どの結果が重要か」という高次の判断に集中する構図です。
数学は人類の知的営みの中で最も厳密さを要求する分野の一つです。その数学において自律的なAIエージェントが証明を完結させたという事実は、「AIはまだ道具だ」という感覚を静かに、しかし確実に塗り替えつつあります。
【用語解説】
可換代数
代数学の一分野。数や多項式を一般化した「環」や「加群」と呼ばれる構造を研究する。乗算の順序を入れ替えても結果が変わらない（可換性）という性質を持つ代数構造を主な対象とし、整数論や代数幾何学などとも密接に関連する。
アンダーソン予想
ダン・アンダーソンが2014年に提起した可換代数上の未解決問題。「予想（conjecture）」とは、正しいと信じられているが数学的に証明されていない命題のことを指す。今回のAIフレームワークが自律的に解決した対象がこれにあたる。
形式検証（形式証明）
コンピューターが一行一行チェックできる厳密な論理言語で数学的証明を記述し、機械的にその正しさを保証するプロセス。「それらしい証明」を生成するだけでなく、誤りの混入を原理的に排除できる点が特徴。
大規模言語モデル（LLM）
GPTやGeminiなどに代表されるAIモデルの総称。大量のテキストデータを学習し、自然言語の生成・理解・推論を行う。数学的証明の生成も可能だが、「ハルシネーション（幻覚）」と呼ばれる事実に基づかない出力を生成するリスクがある。
FirstProof
人間の数学者が解いたが解答が公開されていない問題を収録したAI評価用ベンチマーク。OpenAI・Googleのシステムも挑戦しており、AIの数学研究能力の比較に活用されている。
Aletheia
GoogleがGemini 3 Deep Thinkをベースに開発した数学研究AIエージェント。FirstProofベンチマークで10問中6問を自律的に解いたが、ArchonがLean 4への形式化に成功したProblem 4・6の両問題では解決に失敗している。
【参考リンク】
arXiv｜Automated Conjecture Resolution with Formal Verification（外部）
北京大学チームが2026年4月4日に投稿した本研究の原論文。アンダーソン予想の解決プロセスと詳細な数値情報が記述されている。
Lean 4 公式サイト（外部）
定理証明器兼プログラミング言語Lean 4の公式サイト。数学的証明をコンピューターが検証可能な形式で記述・確認するためのツール。
LeanSearch（外部）
Lean 4のライブラリMathlibの定理を自然言語で検索できるツール。今回のArchonが定理検索に活用した中核的なシステム。
GitHub｜frenzymath/Archon（外部）
形式化エージェントArchonのオープンソースリポジトリ。セットアップ手順が公開されており、外部のAI APIと組み合わせて利用できる。
GitHub｜frenzymath/Rethlas（外部）
非形式推論エージェントRethslasのオープンソースリポジトリ。Archonと連携し、数学的証明の候補を生成する役割を担う。
【参考記事】
Automated Conjecture Resolution with Formal Verification（arXiv）（外部）
本研究の原論文。Problem 4に約50時間・約1,200ドル、Problem 6に約30時間・約750ドルのAPIコストなど、編集部解説で引用した数値の主要な根拠。
Chinese AI solves decade-old maths problem in hours（South China Morning Post）（外部）
2026年4月13日付け報道。アンダーソンの死亡時の年齢や論文公開日など、元記事を補完する背景情報を確認するために参照した。
【編集部後記】
「AIが数学を解く」と聞いて、あなたはどんな感情を抱きましたか？驚き、それとも少しの不安でしょうか。私たちも同じ気持ちで、この研究に向き合いました。AIが証明を「生成」するだけでなく、自ら「検証」する時代に、人間にとって「考える」とはどういう意味なのか——そんな問いをいっしょに持ち続けていけたらと思っています。
