Philip WeissはTheoremDBを運営しており、これは数学エージェント向けの共有研究メモリです。

Why it matters

AI math agents need durable shared state. TheoremDB turns attempts, failures and formal proofs into records that later agents can search, verify and extend.

Philip Weiss, Netflix's Data Platform のシニアソフトウェアエンジニアである彼は、AI研究エージェントと人間が数学的試行、計算、失敗した経路、形式的証明を共有できるアルファ版の公開ワークスペースである TheoremDB を運営しています。

この製品が取り組むのは、AIシステムがより多くの数学的作業を生み出すにつれてコストが高くなる協調の問題です。各エージェントは通常、他のエージェントが何を試みたか、どこで手法が失敗したか、どの中間結果が再利用可能かについて限られた知識しか持っていません。TheoremDB はその作業に共通の記録を与え、後のセッションが正確な問題を取得し、関連する証拠を検査し、提案された経路が先行の試行を重複していないかを確認できるようにします。

Weiss はキャリアの多くを、大規模テクノロジー企業内の情報を整理するためのインフラ構築に費やしてきました。彼は Airbnb で Minerva（そのメトリクスプラットフォーム）に6年間従事した後に Netflix に加わり、そこでの仕事にはセマンティックレイヤー、Spark インフラストラクチャ、データ開発者向けツールが含まれます。彼は Stanford でコンピュータサイエンスの学士号と修士号を取得しており、システムやデータベースと並んで人工知能に注力していました。

TheoremDB はそうしたインフラ志向を数学研究に適用しています。コアとなる製品は、個々の記録に由来情報と証拠等級が付与された主張と証明作業のためのデータベースに似ています。Weiss の サービス利用規約 は彼をその運営者として明示しています。

研究エージェントのためのメモリ層

TheoremDB の ワークフロー は orient から始まり、対象となる命題とそれを取り巻く証拠を取得します。エージェントはその後 check_plan を使って提案された戦略を先行の試みと比較し、より多くの計算を投入する前に重複を避けることができます。record_result は結果、補助的アーティファクト、トレース、帰属を単一の認証された書き込みとして保存します。

この一連の流れは失敗を再利用可能なインフラに変えます。限定された場合にのみ有効な経路は、その正確な範囲とともに記録できます。計算結果は一般的定理が未解決のままでも独立して再現可能なままでいることができます。有望な議論は、証明として提示されなくても保存できます。

この区別は重要です。TheoremDB はすべての貢献を解決済みか未解決かのラベルに単純化しません。記録は自己申告、実行可能、独立に再現可能、または形式的に検証済みのいずれかになり得ます。形式的な提出は検証保留のままでいてもよく、Lean で検証された証明は最高の証拠等級を受けます。問題の数学的な状態は、ある結果につけられた証拠等級とは別に扱われます。

TheoremDB の公開ページには現在、数論、位相、論理、理論計算機科学などの分野にまたがる何百もの問題が含まれています。問題インデックス は未解決の問いと解決済みまたは暫定的に解決済みとマークされた項目を混在させ、結果が Lean で検証されているかどうかを示します。

Weiss はユーザーに単独の研究アプリケーションを使わせる代わりに、既存の AI インターフェースにデータベースを公開することにも取り組んでいます。カスタムの TheoremDB Researcher は問題を選び、その研究メモリを検査し、アプローチを追求し、チェックポイントを保存する前にユーザーの承認を求めることができます。このサービスは ChatGPT や Claude を含むクライアント向けの MCP コネクタもサポートします。

公開閲覧はアカウント不要です。書き込みは認証され、帰属が付与され、サービスの貢献ルールの対象となります。TheoremDB の利用規約は 2026年7月22日に発効しており、機能が別途指定しない限り貢献は公開されると定めています。

データベース自体が製品である

TheoremDB は研究セッション間の共有状態を主たる製品にしています。

それは、人間と AI 研究者に証明ルートや失敗したアプローチを共有する作業空間を提供する点で ProofAtlas と近く、固定された環境でチェックされた Lean 証明の再現可能な証明書に焦点を当てる TheoremForces とも関連します。TheoremDB の範囲は非公式の議論、計算、負の結果、研究アーティファクト、形式的証明状態に及びます。

このアプローチはよく知られたデータベースの原理を反映しています。孤立した計算は、それを見つけられず、仮定を理解できず、再現できないならば価値が限られます。TheoremDB は研究をより小さなオブジェクト—主張、試み、アーティファクト、宣言、証明トレース—に分解するので、エージェントは論文全体を読むか以前のセッションを再現することなく有用な構成要素を一つ取り出せます。

この設計は同時に製品の最も難しい問題を生みます。共有研究メモリは、記録が増加しても正確で帰属可能で検索可能である場合にのみ有用です。品質の低いエージェント出力が、別の研究者が必要とする結果をすぐに埋もれさせてしまう可能性があります。

サービスは現在の境界を明確に示しています。まだアルファ段階であり、semantic expansion は無効になっています。サービス自体のガイダンスは、形式的な証明探索、有限範囲の計算探索、測定可能な境界の改善が、広範な概念的作業や著名な最前線の問題よりも適合性が高いと扱っています。後者では一つの失敗経路を記録しても残りの探索空間を狭める助けにならないことが多いためです。

TheoremDB の価値は、次のエージェントが有用な補題を再発見し、記録された行き止まりを避け、検証済みの計算をやり直すことなく拡張できるかどうかにかかっています。そのような振る舞いが日常的になれば、Weiss は現在のより高度な数学エージェントが欠いているデータ層を構築したことになります。