陶哲軒推出了 Palomar，這是一個旨在作為 Lean 驗證數學論文預印本服務器的新型公開登記處。該平台允許用戶提交符合特定最佳實踐的數學形式化證明，陶哲軒本人也成功提交了其關於 Sendov 猜想的證明作為測試案例。

Palomar 會從源文件的固定版本中記錄數學命題，使用 Lean 檢查證明，並發布精確的命題、庫依賴項以及審查警告。雖然目前依賴 GitHub 來管理身份和垃圾訊息，但它旨在為提交質量設定最低標準。

此舉為形式化證明驗證建立了標準化的基礎設施，彌合了傳統數學與電腦輔助證明系統之間的差距。它為日益壯大的從事複雜理論形式化的 AI 與數學社群提供了一個可靠的儲存庫。

事件背景

Lean 是一款基於歸納演算的證明輔助工具和函數式程式語言，廣泛用於數學的形式化。形式化驗證是指使用軟體來檢查數學證明的邏輯正確性，確保其無誤。在其他證明輔助工具生態系統中，像 Isabelle AFP 這樣的工具早已擔任類似的登記處功能。

社群觀察

社群普遍認為 Palomar 是強化形式化基礎設施的積極一步，並讚賞陶哲軒親民的提交流程。然而，對於其依賴 GitHub 的爭議依然存在，批評者指出它重新製造了 Isabelle AFP 中已有的功能，且存在單點故障的風險。