TheoremGraph: 1800万以上の数学的依存関係を検索
TheoremGraphは、1800万以上の数学的定理とその依存関係を検索可能なグラフ構造のプラットフォーム。数学者や研究者が、定理間の相互参照や証明の依存関係を効率的に探索できる。数理論理学・代数学・解析学など幅広い分野をカバーし、学術研究や教育に活用可能。
背景メモ
米スタートアップTheoremSearchが公開した「TheoremGraph」は、数学の定理・定義・証明間の依存関係（どの定理がどの定理を前提としているか）を検索できるデータベース。18百万以上のエンティティと50百万以上の依存関係をグラフ構造で収録し、ある定理を証明するのに必要な最小限の前提や、逆向きにその定理から何が導けるかを探索できる。形式手法・定理証明支援系（Coq、Lean、Isabelle等）の成果を統合しており、数学の知識体系を機械可読な形で整理する試みの一つ。従来は論文や教科書に散在していた依存関係を横断検索可能にした点が特徴で、数学のカリキュラム設計や自動推論の基盤として注目される。