数学における革新的な予想の発見は、従来専門家の直感と経験に大きく依存してきました。しかし、大規模言語モデル（LLM）の急速な発展に伴い、AIが数学的に意味のある予想を体系的に生成・検証できる可能性が注目されています。このたび研究者らが発表した新しい手法は、まさにこうした課題に取り組むものです。 提案された手法は3段階のパイプラインで構成されています。まず「地域探索」の段階では、具体的な局所証拠モジュールから予想候補を抽出します。次に「反省的検証」の段階では、発見された予想について基礎性、新規性、潜在的重要性を評価します。最後に「形式検証」の段階では、定理証明支援系のLean4とMathlibを用いて、予想の妥当性を形式的に確認します。 このアプローチの目標は、単なる予想の発見ではなく「問題の美しさ」を備えた数学的問題の発見にあります。具体的には、その証明が研究領域の言語体系を再構成し、人間の数学研究に持続的な貢献をもたらす可能性のある問題を対象としています。 実験では20個の候補予想がテストされ、すべてがLean 4のパース処理と型検査に合格しました。また、既存の自動定理証明ツールであるaesopでは直接解決できず、重複や類似する予想も認められませんでした。この成果は、AIが人類の数学的知識の開拓にどれほど貢献できるかを示す重要な一歩となっています。