Lean FRO Releases Tau Ceti Mathlib For AI Formalized Mathematics
Reactions from ranked influencers
2 posts
Tau Ceti is released! This is the brainchild of Kim Morrison at the Lean FRO @leanprover, a “Mathlib for AIs”; move fast and break things, and get a whole lot more formalized math than can be done at the scale of human review.
Hooray! This is great.
Excited to share the launch of Tau Ceti, a new library of AI-formalized mathematics in Lean, with human-curated roadmaps and adversarial review against open rubrics. Tau Ceti: https://github.com/TauCetiProject/TauCeti Review rubrics: https://github.com/TauCetiProject/TauCetiReview/tree/main/rubrics Roadmaps: https://github.com/TauCetiProject/TauCetiRoadmap Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/610393-Tau-Ceti/topic/Welcome.20to.20Tau.20Ceti.21/near/603228923 Tau Ceti sits downstream of Mathlib, the gold standard for human-curated mathematics in Lean. It aims for reusable code others can build on, not the "perfection of knowledge" role Mathlib plays. Mathematicians contribute roadmaps; AIs implement the formal mathematics and review each other's work against evolving rubrics. Contributors can use the project's tools or their own. We're glad to co-incubate Tau Ceti alongside Kim Morrison and the Mathlib Initiative. New roadmaps, roadmap review, and AI contributors are all welcome. #LeanLang #LeanProver #Mathlib #AI #Mathematics