Palomar、AI数学の山積みに対応するためのLean証明レジストリを開設

Why it matters

Palomar gives Lean proofs fixed, commit-level records and separates mechanical verification from semantic LLM review. Its narrow scope provides researchers with an audit trail while explicitly stopping short of peer review.

Palomarは8月18日に投稿受付を開始し、数学者がLeanで書かれた形式的な証明を固定されたソースコードに紐付け、機械的に検証し、初期発表が過ぎ去った後でも検査できる公開レジストリを提供するものです。

Terence Tao、UCLAの数学者で2006年のフィールズ賞受賞者は、ブログ投稿で開設を発表しました。TaoはPalomarの最初の4人の技術メンテナーの一人で、ほかにはMatthew Ballard、Nestor Guillen、およびJaume de Dios Pontがいます。プロジェクトはLean Focused Research OrganizationとInstitute for Computer-Aided Reasoning in Mathematics (ICARM) によってインキュベートされました。

Taoはこのプロジェクトを、Leanで形式化されたものを含むAI生成証明の急増への対応として位置付けました。彼は、そうしたリポジトリをLeanの専門知識を持たない読者が検査することは依然として難しいと書いています：証明は型チェックを通り、無断の公理を含まず、通常の数学的言語で述べられている結果と同じものを形式的に表現している必要があります。

Palomarの解答は、固定されたリポジトリのスナップショットが何を証明しているかというレジストリ記録です。Taoはそれを、Lean証明のためのプレプリントサーバーの「ゼロ次近似」と表現しました。その比較は期待値を適切に設定します。Palomarはインデックス可能な成果物と監査用の記録を作成しますが、数学的内容を査読するわけではありません。

Taoの関与はプロジェクトに可視性を与えますが、Palomarの運営構造は分散化されています。BallardはUniversity of South Carolinaの代数幾何学者です。Guillenは偏微分方程式、変分法、科学計算の分野で活動しています。De Dios Pontは2023年にTaoの下でUCLAの博士号を取得し、NYU Center for Data Scienceの教員フェローとして、調和解析やスペクトル理論と並行して数学のためのAIに取り組んでいます。広範な科学顧問委員会にはJeremy Avigad、Bryna Kra、Kim Morrison、Ravi Vakil、Akshay Venkateshが含まれます。

Palomarが実際にチェックすること

Taoの発表記事は、Palomarを特定のコミットで表される外部GitHubリポジトリのスナップショットのレジストリとして説明しています。各提出には、主張される結果を記述した短いChallenge.leanファイル、証明を含むSolution.leanモジュール、および非公式の説明、メタデータ、開示を含むformalization.yamlファイルが含まれます。

機械的なチェックにはComparatorが使われます。これは広告された主張とその証明を分離し、ソリューションがchallengeファイルの結果を確立しているかどうかを確認するLeanのツールです。Leanのドキュメントによれば、Comparatorは定理の主張の照合をサポートし、Leanのカーネルや独立に実装されたNanodaチェッカーを利用することができます。入手可能な資料からは、PalomarがすべてのComparatorの検証オプションを必須としているかどうかは確定できません。

その分離は微妙な失敗モードに対処します。リポジトリには有効な証明が含まれていても、その形式的な主張がコード外で記述されている定理と異なることがあります。challengeの主張をソリューションから切り離すことで、読者が検査すべき対象が小さくなります。

Palomarの二つ目のチェックは非決定的です。Taoの発表によれば、大規模言語モデルがformalization.yamlの非公式な説明が形式的な結果と一致しているように見えるか、またリポジトリがレジストリの最低基準を満たしているかを評価します。

Palomarの公開ポリシーは自動化された登録レビューについて説明していますが、提供された資料からはメンテナーが別途人手によるモデレーションを行っているかは判断できません。Taoはまた提出時に人間によるレビューを推奨しており、Palomarのチェックは新規性、興味深さ、正確性に関する査読には遠く及ばないと述べています。

したがってこのレジストリは、機械的な証明チェックと、Leanコードと通常の数学的言語との間の意味的橋渡しをモデルに基づいて評価する手続きとを組み合わせています。プロジェクトのドキュメントは、言語モデルによるレビューが不一致を見落とす可能性があると警告しています。読者は定義と形式的主張が論じられている定理を適切に捉えているかどうかを自ら検査する必要があります。

承認を伴わない検証

Palomarはその主張の範囲を明確に区切っています。登録は新規性、重要性、コード品質、あるいは非公式な証明の正しさを認定するものではありません。専門の査読者がその仕事を確認した、という意味でもなく、GitHubリポジトリがジャーナルの出版物になるわけでもありません。

有用な主張は狭義です：指定されたリポジトリのスナップショットからの証明がPalomarの文書化された機械的および自動化されたチェックを通過した、ということです。challengeファイル、ソリューション、および付随する説明は、他の研究者が検査し反論できる材料を提供します。

この区別はAI支援の形式化が広がる中で重要です。証明チェッカーは、コードが符号化された仮定の下で形式的な主張を確立しているかどうかを判断できます。公開された数学的主張はまた、その主張、定義、非公式な説明が同じ結果を指しているかどうかにも依存します。

TaoとPalomarのメンテナーは、レジストリの主張を意図的に限定したまま、その第二の層のためのインフラを構築しています。Palomarは現時点でLeanをサポートしており、提出物は人間が生成したもの、AIが生成したもの、またはその混合によるもののいずれでも構いません。

Palomarは機械生成された数学に関する議論を決着させるものではありません。むしろ、それらの議論に対して固定されたリポジトリのスナップショットと明示的な主張を検査のために提供するものであり、自動化された証明の急増に直面している分野において有用なインフラを提供します。