Palomar Registry Launches as a Preprint Server for Lean‑Verified Mathematics

Palomar provides a lightweight, automated gatekeeper for Lean formalizations

Palomar 是一個新的註冊表，它接受包含 Lean 程式碼的 GitHub 儲存庫快照，檢查形式化陳述是否通過型別檢查（type-check），並使用大型語言模型來比較非形式化描述與所聲稱的結果。機械式檢查（使用 Lean 工具 Comparator）保證了邏輯正確性，而 AI 檢查則為非形式化的主張提供非決定性的健全性測試。Palomar 明確地不進行關於新穎性或趣味性的真人同行評審，這反映了 arXiv 的最低接受標準。

Submission workflow is intentionally rigorous yet achievable

提交流程必須包含：

一個challenge file，包含簡潔、人類可讀的定理（theorem）的 Lean 陳述。
一個solution module，包含完整的 Lean 證明。
一個formalization.yaml 檔案，提供非形式化描述、元數據（metadata）和披露事項。

Tao 成功地透過註冊他自己的 Sendov's conjecture 的形式化證明來展示了這個過程。該註冊表接受來自人類、AI agent 或混合模式的貢獻，現代 AI 助手可以協助提交過程中的機械式面向。

Community reaction highlights strengths and concerns

"The second check (b) is non‑deterministic, being performed by a large language model. Shouldn’t this be just preliminary? I think submissions should have an additional, human‑performed level of verification." – Anonymous comment

"We do not have the resources to host and maintain repositories directly, but would be open to expanding the whitelist of approved repository hosting services beyond Github if there is sufficient demand for doing so." – Terence Tao

"A very quick look at Palomar suggests that it would be much more helpful if each submission required (a) a meaningful Title, and (b) a (well‑written) Abstract explaining what is proved — just as one sees in arXiv." – David Bevan

"Palomar will definitely be something we integrate for data checks and validation" – ygtisik (author of a registry of AI usage in science).

這些評論說明了三個經常出現的主題：

Verification depth – 一些使用者想要在自動化檢查之外增加真人層級的審查。
Repository hosting – 對 GitHub 的依賴被視為單點故障；擴展到其他 git forges 是理想的。
Metadata quality – 更清晰的標題和摘要會提高可搜尋性，類似於 arXiv 的慣例。

Technical design choices and trade‑offs

GitHub‑centric model – 簡化了身份驗證、垃圾郵件控制和版本控制，但會對單一服務產生依賴。正如幾位評論者所提到的，未來的擴展可以將其他替代的 git forges 列入白名單。
AI‑driven semantic check – 提供了一種可擴展的方式來標記形式化陳述與非形式化描述之間的不匹配，但仍具非決定性。註冊表將其視為初步的過濾器，而非最終判斷。
Minimal human involvement – 模仿 arXiv 的方法，讓系統能夠擴展到預期的 Lean formalization 數量，而不需要專門的審查團隊。

Why mathematicians might contribute

Visibility – 條目會出現在可搜尋的註冊表中，賦予作者權限並將形式化內容向更廣泛的社群群體展示。
Reusability – 經驗證的 Lean 證明可以被匯入到其他專案中，減少重複勞動。
AI ecosystem support – 註冊表提供了高品質、機器可檢查的數據，可用於訓練或評估 AI 證明助手。
Community standards – 參與其中有助於塑造 Lean formalization 的最佳實踐慣例。

Comparison with existing efforts

TheoremDB 和 Metamath 已經提供了形式化證明的可搜尋資料庫，但 Palomar 專注於 Lean，並整合了自動化型別檢查加上基於 AI 的語義驗證。
Isabelle AFP 為 Isabelle/HOL 提供了一個長期的存檔，Palomar 可以被視為 Lean 的類似物，儘管仍處於早期階段。

Outlook and open questions

Human‑level validation – 第三方服務可以在 Palomar 的最低限度檢查之上增加同行評審層級。
Metadata enhancements – 在 formalization.yaml 中增加明確的標題和摘要欄位，將使條目符合學術預印本規範。
Hosting diversification – 擴展到 GitHub 之外會減輕對單一平台的依賴，並容以於其他 git forges 使用者。
Incentive structures – 社群正在探索除了聲譽和對可重複使用形式化內容的的渴望之外，還有什麼動機可以驅動貢獻。

Palomar 現在已開放提交。詳細說明可於註冊表的 how‑to‑submit page，討論持續在專屬的 Lean Zulip channel。