Tau Ceti uses AI plus Lean kernel to formalize 'all of basic mathematics', open to contributors
AlexKontorovich · x · 2026-11-03
The Lean team spotlighted Tau Ceti, an AI-driven effort to build a library of formalized mathematics, incubated by Lean FRO and the Mathlib Initiative.
- How it works: human-written roadmaps specify the intended math; the Lean kernel checks every AI-produced proof, and adversarial AI reviewers assess whether definitions/statements match the roadmaps' intent and whether the code is suitable for others to build on.
- Goal: reusable formalizations of "all of basic mathematics", sitting downstream of Mathlib and deferring to its design decisions wherever possible.
- Participating: anyone can "pour in inference" — install the TauCetiWorker (requires a Claude Code or ChatGPT Codex account), and it contributes PRs and reviews others' PRs under your GitHub account, following human-curated roadmaps.
More from coding & agent
- Anthropic and UK AISI report AI agent trying to push malicious code into real open-source repo — LingmingZhang · 2026-11-03
- Best Agentic Apps for Your Phone, November 2026 Edition — Teknium · 2026-11-03
- GitHub Ships Exemption Rules for PR Limits to Auto-Whitelist Trusted Contributors — marlene_zw · 2026-11-03
- Sergey Karayev's loop: Claude Code implements, a QA agent reviews, Claude iterates — sergeykarayev · 2026-11-03
- GitHub Copilot in Teams: @-mention it on an issue and it investigates, fixes, drafts a PR — WirelessLife · 2026-11-03
- Recursive GPT-5-Mini calls often beat a single GPT-5 call for less money — lateinteraction · 2026-11-03