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 是一個社區資源，歡迎所有人的參與。