主要な数学的予想を発見するLLMフレームワーク：AIによる次のリーマン予想への挑戦
このarXiv論文は、大規模言語モデルを用いて主要な数学的予想を系統的に生成・検証する3段階パイプラインを提案し、Lean 4とMathlibによる形式検証を行います。実験では20個の候補予想すべてが構文解析と型チェックを通過し、重複や近似重複も見つかりませんでした。
主要な数学的予想の誕生は、これまで数学者の直感と深い専門知識に依存する、きわめて個人的なプロセスとして知られている。リーマン予想をはじめとする多くの重要な予想は、長年の考察のなかで生まれたものであり、その証明には何十年も要することがある。arXivに投稿された新しい論文「LLM Framework for Discovering Major Mathematical Conjectures: AI's Quest for the Next Riemann Hypothesis」は、このプロセスを大規模言語モデル（LLM）を使って体系的に実行するための3段階パイプラインを提案している。
第1段階は「領域探索（region search）」である。モデルに何もないところから予想を作らせるのではなく、特定の数学分野における明示的な局所証拠モジュールを出発点とする。これらは、その領域ですでに真であることが知られている、または強い根拠がある命題の集まりであり、モデルはこの証拠に導かれながら、その領域内で有望な候補を探索する。第2段階は「再帰的検証（reflective validation）」である。候補は基礎性（foundationality）、新規性（novelty）、潜在的重要性（potential significance）の3つの基準で評価される。これにより、表面的な表現の言い換えではなく、証明されれば研究領域の言語を再編成し、人間の数学研究に永続的な貢献をもたらす可能性のある予想が選ばれる。研究者はこの性質を「問題のセンス（problem taste）」と呼んでいる。第3段階は「形式検証（formal validation）」である。候補はLean 4とMathlibを使って形式化され、自然言語での妥当性だけでなく、機械が検査可能な形で正しく表現されていることが確認される。
実験では20個の候補予想が評価された。結果は次のとおりである。20個すべてがLeanの構文解析と型チェックを通過した。20個すべてがexact?によって直接解決されなかった。20個すべてがaesopによる自動証明で自動的に処理されなかった。また、候補の間に明示的な重複や近似重複も検出されなかった。著者らはこれを「自然言語から形式検査への安定した通過」と表現している。
論文は全25ページ、図1点を含む。著者はAlizer Wong氏ら8名で、2026年4月19日にarXivへ提出された。提出者はZixin Zeng氏で、最初の版（v1）は同日11:13:41 UTCに公開され、ファイルサイズは1,319 KBである。arXiv IDは2607.28632、分類はcs.AI。arXiv発行のDOIは https://doi.org/10.48550/arXiv.2607.28632 で、DataCiteを通じて付与されている。
著者らは、すでに「次のリーマン予想」を発見したとは主張していない。彼らが示したのは、LLMの生成能力と対話型定理証明器の厳密性を組み合わせる枠組みである。この3段階のアーキテクチャは、候補の生成・評価・検証が必要な純粋数学以外の分野にも応用できる可能性がある。AIと形式手法の交差点で働くエンジニアや研究者にとって、この論文は再現可能な方法論と具体的な実験ベースラインを提供している。