Tau Ceti Roadmap

The human-controlled roadmaps for Tau Ceti, an AIs-welcome Lean 4 library downstream of Mathlib. Humans steer the project from here: each roadmap is a markdown README.md, the definitive specification of its area, usually with suggested Lean target signatures in Suggested.lean. The AI-authored mathematics lives in the code repo; review machinery lives in TauCetiReview.

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

Roadmap writing and review can involve a mix of human guidance and AI assistance. Humans direct the mathematical scope and approve roadmap changes; AI can help survey existing libraries, write prose and suggested Lean interfaces, and review the details. If you want to write or review a roadmap, start with Getting started in CONTRIBUTING.md, then read its guidance on writing and reviewing.

Roadmaps

• A statement of the classification of finite simple groups
• Abhyankar's lemma for a regular divisor
• Affine Lie algebras, smooth modules and completed centers
• Algebraic curves: function fields, divisors, and Riemann–Roch
• Algebraic topology of spaces and manifolds
• Algebraic vector bundles
• Amenable groups
• Analytic adic geometry for diamonds
• Analytic families and moduli of complex curves
• Approximation, deformation and rigidity of finite factors
• Banach algebras
• Banach space theory
• Belyi maps, dessins d'enfants, and three-point covers
• Bhargava's mass formula for étale algebras over a local field
• Bordism, formal groups and chromatic operations
• Borel equivalence relations, the G₀ dichotomy and Silver's theorem
• Bounded Laplace and ordered Dirichlet boundary convergence
• Characteristic classes and Chern–Weil theory
• Chevalley groups and the Chevalley–Demazure group schemes
• Class field theory
• Classical arithmetic, sequences, polynomials and reciprocity
• Classification of parabolic subgroups and projective homogeneous spaces
• Classifying spaces of discrete groups
• Clifford bundles, spin structures, and Dirac geometry
• Coboundary expansion with group coefficients
• Combinatorial Heegaard Floer and grid homology
• Compact operators and nonarchimedean Fredholm theory
• Complex manifolds, Dolbeault theory, and Kähler geometry
• Complex manifolds: transport, quotients, bundles, and gluing
• Complex Morse theory, affine topology and weak Lefschetz
• Complex tori: varying lattices and logarithmic transforms
• Computability theory and finite-injury constructions
• Contact homology and the symplectic field theory formalism
• Continuous cohomology of profinite groups
• Counting countable models: Morley's theorem and the Vaught toolkit
• Counting totally ramified extensions of a local field, and Serre's mass formula
• Curvature, Jacobi fields, submanifolds, and Bochner geometry
• Cyclic cohomology, spectral triples and noncommutative tori
• Derived module algebra
• DG and A-infinity algebras, categories, and modules
• Diagrammatic coherence for monoidal categories and duality
• Differential geometry — forms, de Rham cohomology, flows, and degree
• Diophantine approximation and transcendence
• Elliptic analysis of pseudoholomorphic curves
• Elliptic cohomology and topological modular forms
• Elliptic curves
• Elliptic integrals, the AGM, and Jacobi elliptic functions
• Elliptic-curve factorization and Montgomery arithmetic
• Enhanced derived categories of sheaves
• Euclidean isoperimetry, sharp inequalities, and rigidity
• Financial mathematics: one-factor markets and replication
• Finite graph connectivity and network flows
• Finite reflection invariants, degrees, and Weyl exponents
• Finite étale covers of punctured spectra and local purity
• Finiteness and simplicity of the groups on the CFSG list
• Formal Laurent fields, Puiseux expansions and continuous differential calculus
• Foundations of adic spaces, part II — morphisms and analytification
• Foundations of adic spaces, part III — formal geometry, formal models and coherent sheaves
• Foundations of adic spaces, part IV — étale sites, families and dagger geometry
• Four-dimensional Seiberg–Witten theory
• Free groups, equations over groups, and limit groups
• Free probability, free products, and random matrix models
• Fuchsian groups and orbifold Riemann surfaces
• Gaschütz splitting and complements to abelian normal subgroups
• Generalized cohomology, spectra and orientations
• Geometric measure theory: rectifiability, BV, and finite perimeter
• Geometric representation categories and coherent local transport
• Geometric topology and the Kirby-list problems
• Global quadratic forms over number fields
• Graph regularity, finite weak regularity, and arity-3 hypergraph complexes
• Grothendieck groups, Cartan maps, and Euler forms
• Gröbner bases, affine semigroups and algebraic degenerations
• Hamiltonian Floer operations: geometric product and multiplicative PSS
• Heegaard Floer homology, analytically
• Hopfological algebra
• Imaginary quadratic fields: class numbers, finiteness and class number one
• Infinitary model existence, omitting types and interpolation
• Integral currents, geometric homology and minimizing hypersurfaces
• Integral quadratic forms and lattices
• Kac–Moody algebras, integrable modules and path crystals
• Khovanov homology of classical links
• L-functions — completions and functional equations
• Lie algebroids, Lie groupoids and Poisson geometry
• Local variational field theory
• Markov chains and renewal processes
• Modular curves, following Katz–Mazur
• Modular forms — Hecke theory, newforms, and L-functions
• Morse and Floer homology with DG local coefficients
• Morse functions, sublevel topology and Morse–Bott attachments
• Morse–Novikov homology and dynamical Reidemeister torsion
• Neuromanifolds, parametrisations, and neurovarieties
• Newton polygons of polynomials and power series
• Niemeier glue data and explicit Leech constructions
• Nilpotent orbits, Springer resolution and subregular geometry
• Operator theory
• Operator-algebra dynamics, crossed products, and equilibrium
• Optimal transport and Wasserstein geometry
• Orders of the sporadic groups from permutation representations
• P-adic functional analysis
• P-adic measures, completed group algebras, and characteristic ideals
• Partial differential equations
• Perfectoid rings and spaces
• Pivotal and spherical categories
• Positive scalar curvature, surgery and bordism
• Primitive prime divisors and the Bang–Zsigmondy theorem
• Pseudodifferential operators and elliptic analysis on bundles
• Purity of the branch locus
• Quadratic forms and cohomological invariants
• Quantum enveloping algebras of full root data, integral forms and quantum Frobenius
• Quantum groups: compact reconstruction and generic rank-one representations
• Quaternionic analysis
• Random matrices
• Real-analytic geometry and semianalytic triangulation
• Reductive algebraic groups
• Reductive algebraic groups, part II — local structure and arithmetic models
• Representation theory (semisimple algebras, character tables, Lie and classical groups, Schur-Weyl, Peter-Weyl)
• Restricted power series and Tate algebras
• Rigid analytic geometry
• Roth's theorem and the Subspace Theorem over number fields
• Sato hyperfunctions and analytic generalized functions
• Scheme, stack, cohomology and intersection foundations
• Schubert geometry, Demazure sections and flag K-theory
• Smooth orbifolds with finite isotropy
• Smooth principal bundles, connections, and holonomy
• Stable reduction of curves and stable maps
• Stable, periodic, and curved homological algebra
• Standard probability distributions and their elementary theory
• Subfactors, Jones index and planar standard invariants
• Successive minima and Minkowski's theorems
• Symplectic geometry and Hamiltonian mechanics
• Taubes–Gromov theory
• Temperley–Lieb diagrams, categories, and algebras
• The Jacobian challenge
• The Yamabe problem and conformal scalar curvature
• Theta series of lattices
• Topological K-theory of vector bundles
• Topological sheaf cohomology and native comparison maps
• Type-A Hecke algebras, braid traces, and positive quotients
• Von Neumann algebras, factors, and modular theory
• Zeros of L-functions — growth, zero-free regions, counting, and the explicit formula
• Zigzag, preprojective, and Ginzburg algebras
• Étale cohomology foundations

Completed roadmaps

Roadmaps the maintainers have declared complete (a judgment against the roadmap's README.md, the definitive document) are archived and listed in Completed/README.md, outside the active list above.

Generated status files

Each roadmap directory may carry two files that are written by machine, not by hand:

• STATUS.md — a snapshot of where that roadmap stands, rewritten whole on each update and headed by the Tau Ceti commit it describes. It is updated asynchronously from the work it reports, so it is never authoritative about the current tip.
• PROGRESS.md — an append-only log, one section per window of merged pull requests. Each new section is normally announced in the Tau Ceti > Progress logs Zulip topic with links to both the full log and current STATUS.md; announcing is a separate step from merging, so it can fail without holding the report back.

Both are produced by TauCetiProgress. A pull request carrying them can merge without human review, but only when an automated gate accepts it; anything the gate declines is left for a human like any other contribution. Their prose is not security-validated: the gate proves which paths changed and that the log only grew at the end, but it cannot prove that the summary is accurate. Read them as a machine's account of the work, and treat the roadmap README.md beside them — which humans own and review — as the authority on what the roadmap actually asks for.

Writing a roadmap

A roadmap is a specification for material we want added to Tau Ceti, written so an AI contributor, and its reviewers, can act on it without guessing.

• Build the library, don't race to the theorem. For each object you introduce, ask for its complete basic theory, not just the lemma the headline needs. Named theorems are milestones inside a fuller development, not the whole of it. Mario's rule from Mathlib's early days still applies: when you make a definition, it is your job to make it usable, which means the right amount of API. A definition with no lemmas about it is not a contribution.

• No gaps. Every milestone must rest on existing Mathlib or Tau Ceti material, on earlier material in the same roadmap, or on an explicitly cited dependency in another roadmap. Anything else is a leap: a forward reference to a later layer, a connection between two developments that nobody builds, an object named but never made a target. If the roadmap needs something that doesn't exist, building it must itself be a target, here or in a roadmap you cite. The bigger the gap, the worse AIs do with it.

• Every item must be unambiguous. A reasonably clever agent has to be able to work out exactly which definition or theorem you mean, without guessing between candidates.

• Clear boundaries. We keep roadmaps non-overlapping as far as we can, and where one depends on material from another, that dependency is stated. Minimize the number of words a reader needs in order to decide whether something is in scope; jagged boundaries make that impossible.

• Be definite about scope. Nothing is "optional", "deferred" or "for later": don't use the words and don't imply them. Everything on a roadmap is work we want. Sequencing is good, so split into milestones and put the harder material later, but every item lives in some milestone, or a contributor may misread "later" as "never". Decide the generality up front and write it down, rather than recommending intermediate implementations that will be replaced.

• Roadmaps are timeless. They say what we want, not how they came to say it. Don't call an item "blocked" because an earlier roadmap is still being implemented; point at that roadmap instead. When revising, don't leave war stories about why or how the roadmap changed, and don't refer to the review process. Someone reading a year from now should not be able to tell which parts were contentious.

• Aim for reusable material. This one is a should, not a must, but it is what makes a roadmap pay for itself beyond its own headline.

• Deep or broad is up to you. Broad roadmaps are usually better: if we are doing representation theory, let's cover everything taught in graduate classes at more than one university. Breadth makes boundaries easier to draw and optimizes for reuse. But roadmaps also have to motivate people to contribute, and a deep one is sometimes better at that.

Working with Mathlib

• Use Mathlib's vocabulary. Where Mathlib already has a way to say something, use it rather than a private version, both in the roadmap and in the code. A standard notion said in our own dialect drifts from the library it builds on and grows a redundant theory of lemmas Mathlib already proves. For example: Mathlib has no "bounded on a set" predicate, so a result needing an explicit bound carries ∀ x ∈ s, ‖f x‖ ≤ C directly in its hypotheses (as in norm_cfc_le), and uses Bornology.IsBounded when no constant is needed (isBounded_iff_forall_norm_le' relates the two). We do the same, and never wrap a one-line bound in a new predicate. When Mathlib's name is itself a Mathlib-ism a mathematician would not recognize (ModularFormClass, say), link the declaration the first time you use it.

• Defer to Mathlib. Before specifying an object, search Zulip and the open Mathlib PRs for it. Someone may already have formalized it or settled its design. Mathlib owns its API decisions. Tau Ceti adopts the resulting design and refactors when it lands. Cite what you find, follow the direction it takes, and don't argue for a Tau Ceti spelling against Mathlib's.

  Open Mathlib PRs with no substantive development or review activity for six months do not require deference to their proposed APIs. Treat them as prior art: cite and reuse useful work, but choose an appropriate interface for Tau Ceti. Bot updates and mechanical rebases do not reset this period. If the work later lands in Mathlib, adopt Mathlib's API.

• But never wait. Deferring to Mathlib is about shape, never about timing. An active Mathlib PR covering ground a roadmap needs is not a blocker, not a reason to leave a gap, and not a reason to send contributors elsewhere: build the thing here, now, naming and shaping it the way that PR does so the eventual swap is a deletion plus an import rather than a rewrite. If it lands, we delete ours and adopt Mathlib's; if it doesn't, we already have what we needed. Nothing on a roadmap is ever "pending upstream".

• Never push work to Mathlib. Tau Ceti material is built in Tau Ceti and stays there. Plenty of it would make good Mathlib material, and Mathlib contributors are welcome to take any of it at any time, but deciding what Mathlib absorbs is solely theirs. So don't write a roadmap item as "to be upstreamed", don't hold one back because it "really belongs in Mathlib", and don't treat opening a Mathlib pull request as part of discharging a target.

Porting existing work

• Specify the mathematics, not your existing code. Say what each milestone should prove, intrinsically, so a reviewer can judge it on its own terms. A roadmap may direct either a greenfield development or the integration of existing work into Tau Ceti.

• Coordinate first. Work with the authors of the existing material and obtain their agreement before integrating it. If coordination is not possible, do not assume that mathematical overlap permits reuse of their code: verify that its licence permits the intended copying or adaptation, and discuss the plan on the Lean Zulip first. A roadmap that independently develops the same mathematics should still cite the existing work and coordinate where possible, to avoid needless duplication or incompatible design choices.

• Improve it rather than canonizing it. Do not write the roadmap merely to follow the existing formalization; apply all the principles above to make the result more general, reusable and maintainable. Put any file-by-file map in a clearly secondary provenance section, so that nobody treats the source code as prescriptive.

Prototyping

• Write Lean code. It's really helpful to prototype signatures, particularly for structures, classes, and definitions, by writing Lean code, either embedded in markdown or in associated Lean files using sorry. The prototypes are aids, not the specification: the markdown stays definitive, and Suggested.lean is read as suggested forms, never as an exhaustive checklist — open each Suggested.lean with the standard note saying so. Use sorry honestly: a condition you cannot yet even state (its Mathlib API doesn't exist) is still a sorry, never a Prop-typed field or a def _ : Prop := sorry. Both assert nothing (a Prop field is satisfiable by True; a sorry body is sorryAx Prop), so omit a condition you cannot state rather than name an empty one.

• Import existing Tau Ceti APIs. This repository has Tau Ceti as a Lake dependency, so a Suggested.lean file may import individual TauCeti.* modules as well as Mathlib. When an earlier roadmap target is already implemented in Tau Ceti, prototype the new interface against that implementation instead of restating it behind a private stand-in. Import individual modules; Tau Ceti's root module intentionally re-exports nothing.

• Pin conventions. It's essential that you decide conventions ahead of time, or implementors will make bad decisions.

Filing a roadmap

• Give it an arXiv topic. Each roadmap directory holds a metadata.toml with one key, topic: the arXiv math subject class under which a paper proving the roadmap's main results would be listed.

  topic = "math.NT"
  

  Choose the one primary class, as you would for that paper, not every class the material touches. Topics group the roadmaps by area, so that a reader can find the ones in their field. A sub-roadmap is filed under its parent's topic and has no metadata.toml of its own. The build check fails for a roadmap without a valid topic.

How changes are made

Anyone can open a pull request against a roadmap. It merges automatically once it has an approving review from a member of the @TauCetiProject/roadmap-reviewers team (the code owners for roadmap content) and the build check passes. Infrastructure files (the workflows, the Lake config, the toolchain pin) stay with the core @TauCetiProject/humans team.

Rights accrue as you contribute. Opening your first pull request gets you invited to @TauCetiProject/roadmap-triage, which carries triage on this repository: enough to label, assign, and manage issues and pull requests, which is what worker agents need and what a new contributor otherwise lacks. GitHub cannot add you to an organization without your say-so, so watch for the invitation and accept it; triage starts then, not when the PR opens. Landing two merged roadmap PRs then adds you to roadmap-reviewers, so the reviewer pool grows itself out of people who have demonstrably moved a roadmap forward and they can start approving others' roadmap work.

Coordinating work: intentions and claims

To avoid two contributors (human or AI) building the same thing, register what you intend to work on and claim it. This is powered by the intentions bot and the project board.

1. Register an intention. Open an issue with the Intention template: pick the roadmap area and list the specific targets you mean to take (keep the scope as narrow as you can, so the rest stays open for others). Filing it through the API works as well as the web form: title the issue [Intention]: ... and the intention label is applied for you, so no repository permissions are needed.
2. Claim it. Comment claim on the issue. The bot assigns it to you and moves it to Claimed on the board. For a custom window, comment claim 3 weeks or claim 2026-08-01; bare claim uses the project default.
3. It expires. Claims carry a time-to-live (30 days by default, 90 days max) and are released automatically if they go stale, so nothing stays blocked forever. Comment claim again to extend, or disclaim to release early. Opening a PR that says Closes #<issue> advances the card and refreshes the claim; merging it completes the task.

Automated roadmap workers respect these claims: within an area they will not author a target that someone else has claimed. So before a substantial push, register and claim it. A claim is cooperative, not a hard lock; it signals intent so others (people and workers) can steer around you.

Use the Roadmap issue template to report a problem with a roadmap's content, and the Meta template for problems with how this repository operates.

Building

lake exe cache get
lake build