Tau Ceti: An AI-Written Formal Mathematics Library Complementing Mathlib

Uh oh!

There was an error while loading. Please reload this page.

Notifications You must be signed in to change notification settings

Fork 23

Star 111

BranchesTags

Open more actions menu

Folders and files

NameName

Last commit message

Last commit date

Latest commit

History

1,037 Commits

1,037 Commits

.claude

.claude

.github

.github

TauCeti

TauCeti

assets

assets

docbuild

docbuild

scripts

scripts

web

web

.gitignore

.gitignore

AGENTS.md

AGENTS.md

COORDINATION.md

COORDINATION.md

LICENSE

LICENSE

README.md

README.md

TauCeti.lean

TauCeti.lean

formalization.yaml

formalization.yaml

lake-manifest.json

lake-manifest.json

lakefile.toml

lakefile.toml

lean-toolchain

lean-toolchain

Repository files navigation

Tau Ceti is a repository of formal mathematics, directed by human-written roadmaps, implemented and maintained by AI contributors, subject to adversarial review.

Tau Ceti is being incubated by the Lean FRO and the Mathlib Initiative in partnership with academic and industry groups.

Our goal is to formalize as much mathematics as we can in a collaborative, coherent library, at the highest quality we can, subject to the constraint that everything is written by AIs. It's an experiment, and could use your help!

We hope that by building Tau Ceti we can ensure that a significant part of AI formalization work is performed in an open-source, human directed library. Tau Ceti will be built for reuse and generality. Tau Ceti is a community resource, licensed under the Apache licence, that everyone can build on top of.

We've long dreamt about formalizing all the "basic material" in mathematics. While we're explicitly not aiming here at curating and digesting mathematical knowledge in the way that a human authored library like Mathlib can, we hope that we can efficiently build a reusable library at significant scale. With Tau Ceti built, we'll be closer to the point where computers can genuinely help us explore the mathematical universe:

the Lean kernel verifies

the Lean language and user tactics provide automation in proof construction

AIs assist with proof exploration

and Mathlib, Tau Ceti, and other libraries provide the knowledge necessary so that humans can work at the research frontier.

Humans own the roadmap for Tau Ceti, which lives in the TauCetiRoadmap repository (mostly in the form of markdown files, together with a small amount of Lean); changes are made via human-reviewed pull requests there.

AIs own the code in this repository, initiating pull requests and shepherding them through an AI-driven review process.

Humans can raise issues against the code, and leave implementation (and review) to AIs.

(Tau Ceti is a sun-like star about 12 light years from our own, and a favourite setting for sci-fi stories.)

The three repositories

TauCeti (this repository) — the AI-authored Lean mathematics.

TauCetiRoadmap — the human-controlled roadmaps that direct the work.

TauCetiReview — the review rubrics and the machinery that runs review.

Relationship to Lean Pool

Tau Ceti and Lean Pool are complementary. Lean Pool is an arXiv/AfP-like archive of independent formalization projects, whether human- or AI-written. Tau Ceti is an integrated, AI-built mathematical library whose contents follow human-audited roadmaps and undergo review for coherence, reuse, and compatibility with Mathlib.

Review

Review is entirely driven by AIs. These operate according to a fixed open source rubric. Humans write the rubric, and update it as the project evolves.

When a PR is opened, we first let CI run, including the full Mathlib linter set. Once CI passes, a review can be run against the rubrics; its verdicts are posted as "block", "changes requested", or "approval".

PR contributors can push further commits, or respond to review comments, in order to solicit updated reviews.

We've built the infrastructure to fire these reviews automatically on each PR (and on a /review comment), but it is currently switched off. For now, reviews are run from the command line.

You can also run the same review yourself from the command line, on your own Claude and/or Codex subscription instead of the project's metered API budget, using the tauceti-review tool in TauCetiReview. With uv:

print the verdicts for PR #42, posting nothing:

uvx --from git+https://github.com/TauCetiProject/TauCetiReview tauceti-review 42

add --post to publish the scoreboard and per-rubric threads, as you:

uvx --from git+https://github.com/TauCetiProject/TauCetiReview tauceti-review 42 --post

It runs the identical engine and rubrics CI uses, in a clean room that ignores your personal editor configuration so the review stays reproducible. See REVIEWING.md for prerequisites, flags, and the contest/re-review flow.

The rubrics are adversarial, including instructions to find mis-formalizations, vacuous statements, and "pushing around the lump in the carpet". There are rubrics for many different aspects of review — scope, correctness, reuse, attribution, API design, generality, placement, naming, documentation, proof quality, and deprecation; see the rubrics directory. We'll update these as we see what is most useful!

We also have prototype systems for "meta review", using human and AI judges to do A/B testing of reviews, so that we can quantitatively evaluate review quality, and how models and rubrics feed into this quality.

Mathlib dependency

Although Tau Ceti and Mathlib differ both in the review mechanisms and in design standards, and while they target different mathematical goals, we envision a strong synergy between the two libraries. We hope to build overlapping communities around both libraries.

Tau Ceti depends on Mathlib's master branch, and always defers to design decisions made in Mathlib. AIs are encouraged to make PRs to Tau Ceti that bump the pin to new commits on Mathlib's master branch, and fix any resulting problems in Tau Ceti.

We won't push material upstream from Tau Ceti to Mathlib. Mathlib contributors are welcome to adopt, curate, and modify material from Tau Ceti, while preparing PRs to Mathlib. Everything here is Apache licensed.

What Tau Ceti is, and is not

The product of mathematics is clarity and understanding. Not theorems, by themselves. ... There is no way to run out of ideas in need of clarification. The question of who is the first person to ever set foot on some square meter of land is really secondary. --- Bill Thurston

There are many reasons to work on formalizing mathematics, and everyone involved in formalization comes with different reasons. Here are some:

To enjoy the satisfying feeling of the 🎉 emoji when the computer accepts your proof.

To build a modern Bourbaki, digesting and curating mathematical knowledge into a coherent and general form, usable in interactive theorem provers.

To collectively learn how to make best use of, and improve, interactive theorem provers, such as the Lean language.

To participate in a community of like-minded researchers on a common project.

To strengthen trust in the existing mathematical literature, through a combination of audited definitions and theorem statements, and machine verified proofs.

To build a reusable and open library of formal mathematics, that others can freely build on top of.

Tau Ceti is focused primarily on the last point: building an open library, at a quality level sufficient that others can reuse and build on top of it, and at a large enough scale that building on top of it allows downstream projects to reach the research frontier across many areas of mathematics (though, as we discuss below, points 4 and 5 matter to us too).

Tau Ceti is not particularly relevant if you're most interested in 🎉, Bourbaki, and learning how to use and improve Lean itself. Particularly on the Bourbaki front, Tau Ceti is not trying to improve the state of the art for curation, clarity, and understanding: those are explicitly human activities, and should happen in libraries like Mathlib and other human-curated downstream libraries. This is what Mathlib excels at, and is rightly proud of its achievements. Similarly, it seems unlikely that we'll learn much about using and improving Lean while working on Tau Ceti besides, hopefully, some scaling problems! Tau Ceti explicitly sets out to follow Mathlib decisions regarding design and use of language features, because these decisions are hard earned through years of expert usage in formalizing mathematics. We think it's essential that as this knowledge evolves in Mathlib and other libraries, Tau Ceti follows and adapts to these lessons.

We do hope that Tau Ceti will provide a home for many researchers who want to participate in an active and engaging community. It will be a very different process than contributing to libraries like Mathlib. Primarily, the work is to do high level design: learning to write effective and thorough roadmaps, which efficiently lay out the plans to formalize large areas of mathematics well. We'll need deep mathematical expertise in every subject area, and there's a lot of learning to do about how to write roadmaps that produce the best AI output. We're already getting started on these experiments, and Tau Ceti is an opportunity to build a new community around a new kind of formalization work.

Similarly, we expect that Tau Ceti will help build trust in the existing informal literature. Of course, AI formalized definitions are, a priori, untrustworthy, and a big part of the success criteria for Tau Ceti will be in establishing trust from an initially untrustworthy base. We're working on projects to help rapidly audit deep definition chains. Just as in informal mathematics, trust in results isn't really achieved during initial review. We know that results are true only after they've been integrated into a deeper web of mathematics: we've proved more theorems on top of the definitions, and connected the theory to other parts of mathematics. Our hope is that the scale of Tau Ceti will help us achieve that here, and allow the rapid validation of results by building the theory downstream as well.

Collaboration

It's really important we have a good collaboration model with other repositories. We want to make sure that we build rapidly, so that we provide the foundations for people working on frontier research as quickly as possible. But we don't want to get in the way of frontier research, or detract from those efforts.

This will be an evolving process, and community input is welcome. To begin with, our plan is to use the "intentions registration" mechanism from leanprover-community/intentions, and the shared public registry of intentions at leanprover-community/project-intentions.

We already use this mechanism internally so contributors to Tau Ceti can indicate they are actively working on and preparing pull requests for parts of a Tau Ceti roadmap. These intentions are then automatically fed to agents using the ./tauceti worker exemplar from kim-em/TauCetiWorker, instructing them to avoid working on roadmap items claimed by others. We hope that contributors implementing their own workers will also use this mechanism.

We're working now on extending this mechanism to respect recorded intentions at the public project-intentions registry. Hopefully in future there will also be a federated system of registrations collected from individual downstream projects that Tau Ceti can hook into.

(The underlying tooling here was written for earlier projects, but the reusable GitHub Action and the public registry are nice early community benefits from work on Tau Ceti!)

We do want to make some important clarifications about registered intentions, along two axes: frontier vs foundational mathematics, and student projects.

There is so much "frontier mathematics" (roughly, research papers from the last few ye

[truncated for AI cost control]