マサチューセッツ工科大学（MIT）の数学科研究者であるデイビッド・ロウ（David Roe）氏（2006年卒）とアンドリュー・サザーランド（Andrew Sutherland）氏（1990年卒、博士号2007年取得）が、リネッサンス財団とXTXマーケッツが共同で設立した「AI for Math」助成金の初回受賞者に選ばれた。同助成金は、AIを活用して数学的発見を加速する研究を支援するもので、今回29のプロジェクトが採択された。サザーランド氏らと、イースト・アングリア大学のクリス・バーキーブック氏は、大規模な数論データベース「L-Functions and Modular Forms Database（LMFDB）」と、形式証明システム「Lean4」用の数学ライブラリ「mathlib」を連携させるプロジェクトに着手する。 LMFDBは、現代数論の知識を収集した大規模な共同オンラインデータベースで、10億以上の具体的な数学的記述を含む。一方、mathlibは、証明の各ステップを形式的に検証できる「Lean」証明支援システムのためのコミュニティ主導の数学ライブラリで、約10万件の定理や補題を収録している。ロウ氏とサザーランド氏は、LMFDBの未形式化された知識をmathlib内から直接アクセスできる仕組みを開発し、証明支援ツールが特定の証明目標を効率的に探索できるようにする。 「自動定理証明は技術的に難しく、開発資源が不足している」とサザーランド氏。しかし、大規模言語モデル（LLM）の進展により、形式的証明ツールへのアクセス障壁は急速に低下している。今回の連携により、数学研究者が膨大な計算結果を再計算せず、既存のLMFDBデータを活用できるようになる。たとえば、アンドリュー・ワイエルスによるフェルマーの最終定理の証明で使われた「3-5トリック」のように、非自明な計算を必要とする証明の一部でも、既に計算済みのデータを活用できる。 さらに、数学データベースはランダムな情報集ではなく、専門家が選別・整備した信頼できる知識の集積である。サザーランド氏は、機械学習を用いた「murmurations」の発見が、楕円曲線の「導手（conductor）」の重要性を強調するデータの活用に起因したと指摘。今後の計画として、楕円曲線、数体、モジュラー形式の定義を形式化し、mathlib内からLMFDBの検索を可能にする開発チームの構築を進め、MITの学生も参加を呼びかけている。