近幾個月來，各種新舊結果的 AI 生成證明激增，其中一些已在證明輔助語言 Lean 中形式化。然而，要驗證一個給定的 Lean 儲存庫是否確實證明了聲稱的陳述，對於不熟悉 Lean 使用的讀者來說，是相當不簡單的：首先必須檢查聲稱的 Lean 形式陳述是否能成功編譯，證明中是否包含任何「作弊」行為（例如添加額外公理），以及形式陳述在語義上是否與聲稱結果的非正式描述相符。
為了為此情況帶來一些清晰度，我很高興地宣布，Palomar：一個 Lean 驗證數學的註冊中心，這是一個由 Lean FRO 和 ICARM 孵化的計畫，現已開放提交。我將在這個註冊中心擔任多個角色，包括科學諮詢委員會成員，與 Jeremy Avigad、Matthew Ballard、Jaume de Dios、Nestor Guillen、Bryna Kra、Kim Morrison、Ravi Vakil 和 Akshay Venkatesh 一同服務。
關於 Palomar 的詳細動機可以在這裡找到，更多關於 Palomar 的資訊可以在這裡找到。Palomar 的一個零級近似是 Lean 證明的預印本伺服器。更精確地說，Palomar（以天文觀測站命名）是一個外部 Github 儲存庫的註冊中心（更準確地說，是這些儲存庫的「快照」，由特定的 Github commit 代表），其中包含符合此類形式化當前最佳實踐的 Lean 代碼，特別是包含
（儲存庫還有一些額外的技術要求，我將在此省略。）如果儲存庫的快照被提交到 Palomar，它將檢查（a）解決方案模組是否能成功編譯並準確證明挑戰檔案中聲稱的結果，以及（b）formalization.yaml 檔案中的結果非正式描述是否與挑戰檔案中聲稱的結果相符，並且儲存庫是否符合註冊條目所需的各種最低標準。第一個檢查（a）是純粹機械化的，使用 Lean 工具 Comparator；第二個檢查（b）是非確定性的，由大型語言模型執行。如果一個儲存庫通過了這兩項檢查，它就可以在 Palomar 註冊。值得強調的是，檢查（a）和（b）遠遠不足以進行對提交內容的新穎性、趣味性和準確性的嚴格人類同行評審；特別是，Palomar 並非同行評審期刊。
提交過程雖然嚴謹，但卻是可行的：作為測試，我成功地將我最近對 Sendov 猜想證明的形式化提交到了 Palomar，並且也計劃很快將一些較舊的形式化提交到該註冊中心。
總之，該註冊中心現已開放提交對新舊結果的形式化。歡迎提交（無論是人類生成、AI 生成，還是兩者混合）；請在開始提交前閱讀（相當詳細的）說明。 （不過我會注意到，現代 AI 代理在協助處理提交的機械細節方面非常有用，但仍然強烈建議進行人工審查。）
關於 Palomar 的討論和回饋將在這個 Zulip 頻道進行。