Tau Ceti

Tau Ceti, read at commit ace60277 (2026-11-07), with its roadmaps at eaf17b10: 2,809 articles on 3,906 of its declarations, in parts by the library's top-level areas. 1,377 are the declarations a roadmap's status names as a result or a notable definition. A model writes the statuses and names at most five results in each, so the other 2,529 are results Tau Ceti's own docstrings name: a theorem whose docstring opens with a bold title naming a result after a person ("Burnside's pᵃqᵇ theorem", "Schur-Weyl duality", "Hille–Yosida"), a title such as "The cellular approximation theorem", or a short title pinned to a textbook theorem; a definition that carries such a theorem as data; and the four theorems Tau Ceti's website shows. The forms of one result in one area share an article. The 11 names the statuses give that Tau Ceti does not have at this commit have no article. A roadmap's plan, its suggested signatures and its frontier say what Tau Ceti may add, so they are left out, and so is the statuses' prose: a model writes it, and Tau Ceti does not check it.

Each of the 126 roadmaps whose status names a declaration has a section, in the part where most of its articles are. It holds what the status names and the other named results near them: those in a module where no other roadmap's status names a declaration, or else in a folder of modules below the areas where this status names at least 2 declarations and no other names any. The other named results are in 133 sections by area, a module's first two levels under TauCeti; an area with fewer than 3 of them joins its part's Other results, and a part with fewer than 10 articles joins Other Areas.

Each article's text is its declaration's docstring and signature, under Tau Ceti's Apache-2.0 license; a docstring that opens with a bold title, or with bold words its first sentence goes on from, gives the article its title. Dependencies come from Tau Ceti's declarations (lean/tauceti/TauCetiDeps.lean): under Depends on, the articles that a statement reaches through the statements of declarations not mapped here, and under Proof depends on, those a proof reaches through any chain of Tau Ceti declarations not mapped here. A theorem or definition that reaches sorry, itself or through a declaration mapped here, says so, and one stated from a proposition Tau Ceti defines says what it assumes.

• Algebra
• Algebraic Geometry
• Algebraic Topology
• Analysis
• Category Theory
• Combinatorics
• Field Theory
• Geometry
• Group Theory
• Knot Theory
• Linear Algebra
• Measure Theory
• Model Theory
• Number Theory
• Probability
• Quantum Groups
• Representation Theory
• Ring Theory
• Topology
• Other Areas

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.