テリー・タオ氏が、数学者やプログラマーと共に作成した概念実証ツールについて報告しました。このツールは、特に大規模パラメータに対する不等式の検証を自動化することを目的としています。具体的には、加算、乗算、除算、累乗、最小値、最大値などによって組み合わされた有限個の正の実数に対する不等式を自動的に検証します。たとえば、弱い算術平均-幾何平均不等式： [ (a \cdot b \cdot c)^{1/3} \lesssim \max(a, b, c) ] ここで (a, b, c) は任意の正の実数であり、(\lesssim) は未知の定数倍を許すことを示します。この不等式は、最大値を考慮するために3つのケースに分割して検証されます。各ケースでは、与えられた前提条件から不等式の正しさを自動的に決定し、証明または反例を提供します。 この概念実証ツールは、Pythonで4時間程度で開発されました。大型言語モデル（LLM）の助けを借りてコードを生成し、自動完成させました。現在、基本的な変数のみを扱う前提条件には対応していますが、より複雑な式にも部分対応しています。例えば、次の論文での不等式を検証するためのコード： [ \left( \frac{M_1 + M_2}{2} \right)^{1/2} \lesssim \max(m_1, m_2, M) ] ここで (M_1, M_2, m_1, m_2, M) は適切な制約条件下にある最大値、中央値、最小値を表しています。このような不等式は、手動でチェックすると時間がかかりますが、自動ツールがあれば効率的に検証できます。 タオ氏は、このツールが将来的にはより高度な課題に対処できる可能性があると見込んでいます。例えば、多線形積分を標準的な空間（ソボレフ空間など）のノルムで推定することや、AIの提案に基づいて和や積分の分割を自動化することなどが考えられます。また、証明を形式化するために Lean などの助言言語出力機能の追加も提案されています。 科学技術コミュニティでは、この種の自動化ツールの重要性が認識されており、共同プロジェクトとして発展していくことを期待しています。既存のプラットフォーム（例如、SageMATH）に統合することや、特定のツールセットで最適な推定を行い証明する機能などが最も有望だとされています。このツールが数学の研究を大幅に支援することに大きな可能性があります。 数学の専門家たちは、複雑な計算を自動で行い、手間を省くことで研究の効率化を望んでいます。タオ氏は、この概念実証ツールを通じて、より洗練された自動不等式検証ツールの開発が近い将来可能ですとの見解を示しました。