Tau Ceti：AI編寫的形式化數學庫，與Mathlib互補

Tau Ceti 是一個由人工智慧驅動的形式化數學庫，由 Lean FRO 和 Mathlib Initiative 聯合孵化，並與學術界和工業界合作。該專案的一個核心特點是，人類數學家負責制定路線圖，而 AI 系統則根據這些路線圖編寫程式碼。所有貢獻都透過 AI 驅動的審查流程，審查規則由人類編寫並公開在 TauCetiReview 倉庫中。Tau Ceti 與 Mathlib 的關係是互補的：它建立在 Mathlib 的基礎上，但更注重快速構建可重用的數學庫，而非精細的整理和消化。專案的目標是透過大規模的形式化工作，為前沿數學研究提供基礎。

審查過程是敵對的，旨在發現錯誤或空洞的陳述，確保質量。AI 根據固定的開源規則進行審查，當 PR 開啟時，先執行 CI（包括完整的 Mathlib 程式碼檢查），然後根據規則給出“阻止”、“請求更改”或“批准”的判決。目前審查基礎設施已搭建但尚未自動觸發，可以透過命令列執行。此外，專案還引入了“元審查”系統，使用人類和 AI 評委對審查進行 A/B 測試，以量化評估審查質量。

Tau Ceti 依賴於 Mathlib 的主分支，並始終遵循 Mathlib 的設計決策。AI 被鼓勵提交 PR 來更新 Mathlib 的依賴並修復相關問題。專案不會將材料向上遊推送到 Mathlib，但 Mathlib 貢獻者歡迎採用、整理和修改 Tau Ceti 的材料。所有程式碼採用 Apache 許可證。

該專案明確不旨在像 Mathlib 那樣進行精細的策展和整理，而是專注於構建一個可重用、大規模的開放庫。Tau Ceti 的哲學是，數學的產物是清晰和理解，而非僅僅定理本身。專案希望透過在 Tau Ceti 上構建下游形式化來逐步建立對 AI 編寫定義的信任。信任不是透過初步審查實現的，而是透過將定義整合到更深的數學網路中，並在其之上證明更多定理來建立的。

在協作方面，Tau Ceti 使用“意圖註冊”機制，允許貢獻者宣告他們正在積極工作的路線圖部分，從而避免重複勞動。該機制已內部使用，並計劃擴充套件到公共專案意圖註冊中心，未來可能實現聯邦系統。專案強調快速發展，為前沿研究提供基礎，同時不干擾這些研究。Tau Ceti 是一個社群資源，歡迎所有人的參與。