Tau Ceti: Building a Mathematical Library with AI and Lean

Contributed by Kim Morrison

Tau Ceti is using AI to build a library of formalized mathematics. Human-written roadmaps specify the intended mathematics, and Lean’s kernel checks every proof the AI contributors produce. Adversarial AI reviewers then assess whether the definitions and statements match what the roadmaps intend, and whether the resulting code is suitable for others to build on.

The Tau Ceti project is currently incubated by the Lean FRO and the Mathlib Initiative.

The Goal: All of Basic Mathematics🔗

The goal is to quickly provide reusable formalizations of "all of basic mathematics", i.e. everything needed so researchers can build on top of Tau Ceti to reach the research frontier. Tau Ceti lives downstream of Mathlib, which is the gold standard of formal mathematics. Wherever possible, Tau Ceti defers to Mathlib’s design decisions, and when material that started in Tau Ceti is later formalized in Mathlib, Tau Ceti’s default is to switch promptly to the Mathlib version.

Getting Started🔗

Tau Ceti is designed so everyone can just "pour in inference". Getting started can be as simple as

uv tool install git+https://github.com/kim-em/TauCetiWorker.git
gh auth login        # the worker acts as this account, and tends its PRs
tauceti doctor       # checklist of everything it needs
tauceti work --loop  # prepare PRs, and review other contributors' PRs

(This assumes you're in a shell with an authenticated Claude Code or ChatGPT Codex account.)

In the default mode, this Tau Ceti "worker" will contribute to reviewing incoming Tau Ceti pull requests, and generate new pull requests formalizing mathematics according to existing roadmaps.

These roadmaps are coordinated by the human architects of Tau Ceti: everyone can propose new roadmaps, and participate in their curation.

Progress So Far🔗

Tau Ceti is growing fast, and the evidence so far is that it is "good enough": even though all the material is AI generated, the adversarial AI review process brings the material up to a standard we can keep building on. We think that within a year or two Tau Ceti can contain a substantial fraction of graduate-level mathematics, providing all the reusable pieces needed to perform mathematical research across a very broad range of topics.

Recent results include:

  • Burnside's theorem: every finite group whose order has at most two distinct prime factors is solvable.

  • Carathéodory's boundary extension theorem: a conformal map from the unit disc onto a Jordan domain extends to a homeomorphism of their closures.

  • Schur–Weyl duality: on tensor powers, the images of the general linear and symmetric group algebras are each other's centralizers, over an infinite field in which the factorial of the tensor degree is nonzero.

Get Involved🔗

We invite collaboration and contribution from everyone: