Palomar：Leanで検証された数学の登録簿が公開

Palomar: A registry of Lean verified mathematics

Terence Tao氏は、Leanで形式化された数学の証明を登録するためのレジストリ「Palomar」の開設を発表した。Palomarは、AI生成の証明が増える中で、証明が実際に主張を検証しているかを確認する仕組みを提供する。登録には、チャレンジファイル、ソリューションモジュール、formalization.yamlファイルが含まれ、機械的なチェックとLLMによる意味的整合性のチェックが行われる。査読付きジャーナルではないが、証明の信頼性を高めるための一歩となる。