Palomar レジストリが Lean で検証された数学のプレプリントサーバーとして登場

Palomar は軽量で自動化された Lean 形式化のゲートキーパーを提供

Palomar は、Lean コードを含む GitHub リポジトリのスナップショットを受け入れ、形式的な命題が型チェックされるかを確認し、大規模言語モデルを用いて非形式的な記述と主張された結果を比較する新しいレジストリです。機械的な検証（Lean ツール Comparator を使用）により論理的正しさが保証され、AI 検証は非形式的主張に対する非決定論的な健全性テストを提供します。Palomar は明確に 人間による査読（新規性や興味の有無について）を行わず、arXiv の最小限の受入基準を模倣しています。

提出ワークフローは意図的に厳格でありながら達成可能

提出には以下のものが必須です：

challenge file：定理の簡潔で人間が読みやすい Lean 表記。
solution module：完全な Lean 証明を含むモジュール。
formalization.yaml ファイル：非形式的な説明、メタデータ、開示事項を提供。

陶は、自身の Sendov の予想の形式化証明を成功裏に登録することで、このプロセスを実証しました。レジストリは人間、AI エージェント、あるいはハイブリッドからの貢献を受け入れ、現代の AI アシスタントは提出の機械的側面を支援できます。

コミュニティの反応から強みと懸念が浮き彫りに

"2 番目のチェック（b）は大規模言語モデルによって非決定論的に行われます。これはあくまで予備的なものにすべきではないでしょうか？提出物には追加で人間による検証レベルが必要だと思います。" – 匿名コメント

"私たちはリポジトリを直接ホスト・維持するリソースを持っていませんが、需要があれば GitHub 以外の承認済みリポジトリホスティングサービスのホワイトリストを拡張することにオープンです。" – Terence Tao

"Palomar を少し見てみたところ、各提出物に（a）意味のあるタイトル、および（b）よく書かれた要約（abstract）を要求するほうがはるかに役立つように思われます。arXiv で見られるようにです。" – David Bevan

"Palomar は確かにデータの検証と検証のために統合する予定です" – ygtisik（科学における AI 利用のレジストリの作成者）

これらのコメントは以下の3つの繰り返されるテーマを示しています：

検証の深さ – 自動検証を超えた人間によるレビュー層を求めるユーザーがいる。
リポジトリホスティング – GitHub への依存は単一障害点と見なされ、他のフォークへの拡張が望まれる。
メタデータの質 – 明確なタイトルと要約があれば、arXiv の慣習に合わせて検索可能性が向上する。

技術的設計選択とトレードオフ

GitHub に依存するモデル – ID、スパム制御、バージョン管理を簡素化するが、単一サービスへの依存を生む。複数のコメントで指摘されたように、将来の拡張として他の Git フォークのホワイトリスト化が可能である。
AI による意味的検証 – 形式的命題と非形式的記述の不一致をスケーラブルに検出できるが、非決定論的である。レジストリはこれを最終判断ではなく、予備フィルタとして扱う。
最小限の人間参加 – arXiv のアプローチを模倣し、専任の査読チームなしで、予想される Lean 形式化の量にスケーラブルに対応できる。

数学者が貢献する理由

可視性 – エントリは検索可能なレジストリに掲載され、著者に評価が与えられ、形式化が広いコミュニティに露出する。
再利用性 – 検証済みの Lean 証明は他のプロジェクトにインポート可能で、作業の重複を減らす。
AI エコシステム支援 – レジストリは高品質で機械検証可能なデータを提供し、AI 証明アシスタントの訓練や評価に役立つ。
コミュニティの基準形成 – 参加することで、Lean 形式化のベストプラクティスの慣習を形作る手助けになる。

既存の取り組みとの比較

TheoremDB と Metamath は既に形式証明の検索可能なデータベースを提供しているが、Palomar は Lean に特化しており、自動型チェックと AI を用いた意味的検証を統合している。
Isabelle AFP は Isabelle/HOL 用の長年のアーカイブを提供している。Palomar は Lean 版の類似物と見なせるが、まだ初期段階にある。

今後の展望と未解決の問い

人間レベルの検証 – 第三者サービスが Palomar の最小限のチェックの上に査読を重ねられるようにする。
メタデータの強化 – formalization.yaml に明示的なタイトルと要約フィールドを追加することで、学術的なプレプリントの慣習に沿う。
ホスティングの多様化 – GitHub 以外への拡張により、単一プラットフォームへの依存を軽減し、他のフォークを利用しているユーザーにも対応できる。
インセンティブ構造 – 評判や再利用可能な形式化の欲求を超えた貢献を促す動機は、まだコミュニティが模索中である。

Palomar は現在、提出を受付けています。詳細な手順はレジストリの提出方法ページに、議論は専用の Lean Zulip チャンネルで継続されています。