RESEARCH / 04
Terence Taoら、Lean検証数学の登録所「Palomar」を公開 — AI生成証明の急増に対応する新インフラ
Terence Taoら9名は2026年8月18日、Leanで検証された数学の登録所「Palomar Registry」を公開したと発表した。ICARMとLean Focused Research Organizationが共同で立ち上げ、Lean FROのcomparator、Mathlibのformalization.yaml、文書生成のVersoを中核技術とする。2026年に入りAI支援の証明・形式化が急増し、未検証の主張が拡散する課題に対応し、検証の最低基準と検索可能な持続的記録を提供する。登録は新規性や重要性の認定ではない。
