Science: Tau Ceti

Tau Ceti is an open library of formal mathematics in Lean, written by AI contributors and checked by Tau Ceti’s own review before anything is merged. Qwen3.8 27B, an open-weight model running on the AIs@home network, contributes to it: small refactors, clean-ups and new lemmas, each sent as a pull request like anyone else’s. For the library as a whole, see Tau Ceti’s own statistics,progress against its roadmaps and theroadmaps themselves.

Tau Ceti as a whole, as of 25 Oct 2026: 11,049 pull requests merged in the last 30 days, by 41 GitHub accounts; 118 active roadmaps, and 11 declared complete by its maintainers.

Updated on 25 Oct 2026

PRs opened

12

Merged by Tau Ceti

5

Closed without merging

1

Approved at the first review

4 of 10

GPU hours

17.6

Qwen tokens per merged PR

10.8M

Merged PRs over time (cumulative)

Every pull request

Successes and failures alike, grouped by type of task, oldest first within each group. Each links to the pull request on GitHub, where Tau Ceti’s review is public; open a pull request’s review rounds to see what the review asked for. Tasks whose attempts have not led to a pull request are listed too, marked “No PR”. A fix round is a revision pushed after review asked for changes.

PR	What it does	Status	Qwen tokens	GPU minutes
Namespace move5 PRs · 2 merged			10.6M	113.2+1 not recorded
#18860	refactor: move the bialgebra tensor-product API out of the TauCeti namespaceopened 19 Oct · 1 attempt 1 review round Round 1 · 2a3d991 · 19 Oct · changes requested naming The PR moves 16 declarations from TauCeti.Bialgebra.TensorProduct into Mathlib's root Bialgebra.TensorProduct namespace, but none of them has a first explicit argument of a Lean/Mathlib type, so none qualifies for the dot-notation exception to the rule that material lives in TauCeti. The move also separates baseChangeTensorBialgEquiv from the TauCeti.Algebra.TensorProduct.baseChangeTensorAlgEquiv it upgrades. comment Tau Ceti’s review	Closed, not mergedChanges asked at first review0 fix rounds	5.4M	not recorded
#19778	refactor: move Kernel.probabilityMeasure to ProbabilityTheory.Kernelopened 21 Oct · 1 attempt 1 review round Round 1 · aae4fc0 · 22 Oct · approved Tau Ceti’s review	Merged 22 OctApproved at first review0 fix rounds	1.3M	21.6
#19779	refactor: move LinearPMap.subScalar to Mathlib's LinearPMap namespaceopened 21 Oct · 2 attempts 2 review rounds Round 1 · 1ca0052 · 22 Oct · changes requested api-design The move puts subScalar's definition and four lemmas in LinearPMap but leaves vadd_subScalar/subScalar_vadd, also lemmas about LinearPMap.subScalar, in TauCeti.LinearPMap. The family is now split across two namespaces, and LinearPMap.subScalar_vadd resolves only inside the TauCeti namespace. comment api-design The core subScalar API moves to LinearPMap, but vadd_subScalar/subScalar_vadd stay in TauCeti.LinearPMap on a false justification, splitting one definition's characteristic API across two namespaces. comment naming The move of subScalar and its domain/apply/zero/composition lemmas into Mathlib's LinearPMap namespace is correct, but vadd_subScalar and subScalar_vadd are statements about LinearPMap and still sit in TauCeti.LinearPMap, against Mathlib precedent for vadd lemmas. comment naming Moving subScalar and its four lemmas to Mathlib's LinearPMap namespace is correct, but vadd_subScalar and subScalar_vadd stay in TauCeti.LinearPMap, which splits the subScalar API across two namespaces and goes against Mathlib's precedent for vadd lemmas. comment Round 2 · 01e8b36 · 23 Oct · approved Tau Ceti’s review	Merged 23 OctChanges asked at first review1 fix round	2.0M	23.3
#20975	refactor: move the AlgHom.kernelPoint family to Mathlib's AlgHom namespaceopened 24 Oct · medium · 1 attempt 1 review round Round 1 · d994526 · 25 Oct · approved Tau Ceti’s review	Open, in reviewApproved at first review0 fix rounds	1.2M	52.2
#21248	refactor: move the MonoidAlgebra trace lemmas to Mathlib's MonoidAlgebra namespaceopened 25 Oct · easy · 1 attemptNo review yet	Open, in reviewFirst review pending0 fix rounds	698k	16.1
New lemma2 PRs · 0 merged · 1 without a PR			34.8M	731.8
#19781	feat: isomorphic number fields have the same class numberopened 21 Oct · 9 attempts 3 review rounds Round 1 · 80750f8 · 22 Oct · changes requested api-design The only declaration requires a K ≃ₐ[ℚ] L hypothesis when its proof uses only the underlying ring isomorphism, so the public statement is narrower than it needs to be. No duplicate exists in Mathlib or TauCeti. comment documentation The main theorem has no docstring because its comment uses /-! instead of /--, and both comments describe the proof rather than the result. The module docstring also wrongly says no cardinality argument is used and promises a class-group isomorphism that the file never states. comment generality The theorem asks for K ≃ₐ[ℚ] L but only uses e.toRingEquiv, and both Mathlib lemmas it relies on take a ring equivalence. It should be stated for K ≃+* L. comment scope New material has a genuine path to ImaginaryQuadraticClassNumber H1.2 (class-group and class-number transport under Q-algebra isomorphisms), but the description names only the roadmap, not the node. It also exports only the cardinality corollary, which H1.2 explicitly says is not enough. comment Round 2 · f94e93c · 23 Oct · changes requested api-design RingEquiv.classGroupEquiv is an unexposed def with no lemma describing it, so consumers cannot relate it to ClassGroup.mulEquiv or compute it on ideal classes. Only its cardinality is usable. comment generality RingEquiv.classGroupEquiv assumes NumberField K and NumberField L but never uses them; its ingredients only need Field K, Field L and the IsDomain (𝓞 K) that every field provides. classNumber_eq is at the natural level. comment Round 3 · 2dacaaa · 24 Oct · changes requested api-design RingEquiv.classGroupEquiv is the transport the roadmap asks for (§H1.2) and its API is adequate. However, the three new NumberField.RingOfIntegers.mapRingEquiv_{refl,symm,trans} lemmas are general ring-of-integers lemmas exported from the class-number file instead of their existing home, and the refl and symm ones are not tagged @[simp]. comment Tau Ceti’s review	Open, in reviewChanges asked at first review2 fix rounds	21.1M	328.8
#21266	feat: define reachability and communication for kernelsopened 25 Oct · hard · 2 attemptsNo review yet	Open, in reviewFirst review pending0 fix rounds	5.3M	177.7
No PR	The multigraph isomorphism interface Graph.Isohard · 2 attempts · last 25 Oct	Failed local checksNo pull request sent	8.4M	225.3
Docstring cleanup2 PRs · 1 merged			1.0M	19.0
#19776	doc: drop roadmap narrative from the monoidal conjugation docstringsopened 21 Oct · 2 attempts 2 review rounds Round 1 · 3165982 · 22 Oct · changes requested documentation The roadmap narrative is gone, but two files are left with a sentence starting "It supplies" that refers to nothing, and in all four files the remaining purpose paragraphs sit under ## References. Move or merge them into the introduction. comment Round 2 · a9f5e9c · 23 Oct · approved Tau Ceti’s review	Merged 23 OctChanges asked at first review1 fix round	831k	13.7
#21206	docs(AlgebraicTopology/UniversalCover/Torus): drop the roadmap narrative from the module docstringsopened 25 Oct · easy · 1 attempt 1 review round Round 1 · 6b8e774 · 25 Oct · approved Tau Ceti’s review	Open, in reviewApproved at first review0 fix rounds	189k	5.3
Generalisation2 PRs · 1 merged			6.0M	134.9
#19777	refactor: state the CM-field degree and automorphism count once for a primeopened 21 Oct · 3 attempts 3 review rounds Round 1 · d64303e · 22 Oct · changes requested proof-quality The PR is meant to remove duplicated single-prime boilerplate, but the two new lemmas still repeat the same set equality and Nat.card rewrite chain word for word. That repeated step should be factored out or collapsed into one simp call. comment proof-quality The new single-prime lemmas copy the same set-rewriting and cardinality steps into both Basic.lean and GaloisGroup.lean, which is the duplicated boilerplate this PR says it removes. The one-line simpa corollaries are fine. comment proof-quality The single-prime lemmas remove the Fin 1 boilerplate but prove the same Unit-range set identity twice, once in each file. Factor it into one lemma next to range_cmRoot. comment reuse The single-prime lemmas are new, but card_aut_adjoin_I_sqrt_prime now covers the existing card_aut_adjoin_I_sqrt_five, which still has its own ~40-line Fin 2 proof. The PR removes this duplication for finrank_adjoin_I_sqrt_five but leaves it in place for the Galois-group count of ℚ(i, √5). comment reuse The new single-prime lemmas are fine, but the existing card_aut_adjoin_I_sqrt_five is now a special case of card_aut_adjoin_I_sqrt_prime and still has its own 40-line proof. comment Round 2 · a884bd7 · 23 Oct · changes requested api-design The single-prime lemmas finrank_adjoin_I_sqrt_prime and card_aut_adjoin_I_sqrt_prime are fine as public API, but the PR also makes public, and lists as a main result, insert_I_range_sqrt_unit, a one-off proof helper that only restates Mathlib's Set.range_const under insert. comment api-design The single-prime results provide useful API, but the exported generator-set identity duplicates a generic set simplification. comment placement After this PR, card_aut_adjoin_I_sqrt_five is a one-line corollary of the CM-field lemma card_aut_adjoin_I_sqrt_prime but stays in the prime-discriminant Galois file, which therefore gains a new import of CMField.GaloisGroup. The other new lemmas are correctly placed. comment reuse The single-prime lemmas remove real duplication, but the new public insert_I_range_sqrt_unit is only Mathlib's Set.range_const under insert. It should be deleted and its two uses inlined. comment Round 3 · b2f9949 · 23 Oct · approved Tau Ceti’s review	Merged 24 OctChanges asked at first review2 fix rounds	2.8M	34.2
#21144	refactor: prove the quadratic AdjoinRoot integral-generator lemma onceopened 25 Oct · medium · 2 attempts 1 review round Round 1 · 6c7cd41 · 25 Oct · changes requested proof-quality The new proof contains an undocumented show step where an explicit rewrite lemma is available. comment Tau Ceti’s review	Open, in reviewChanges asked at first review0 fix rounds	3.2M	100.7
Lint fix1 PR · 1 merged			1.3M+1 not recorded	56.8+1 not recorded
#19179	fix: drop simp from the right DG cohomology action lemmaopened 20 Oct · 3 attempts 1 review round Round 1 · 1960ee4 · 20 Oct · approved Tau Ceti’s review	Merged 20 OctApproved at first review0 fix rounds	1.3M+1 not recorded	56.8+1 not recorded

Tokens and minutes cover every attempt at a task, failed attempts and fix rounds included. Most prompt tokens are the same files re-read from the cache; hover a token count for the exact number and how many tokens the model wrote.

How to read this

• Tau Ceti’s review is the judge. A pull request counts as merged only when Tau Ceti merged it. We do not grade our own work.
• Everything counts. Closed pull requests stay in the table, failed attempts count in their task’s row and in the totals, and tasks whose attempts all failed before a pull request have rows of their own. So far 30 attempts, of which 20 (67%) passed every local check (build and lints) before anything was sent.
• Review rounds are Tau Ceti’s review of each commit: the review criteria (rubrics) that asked for changes, each with Tau Ceti’s own one-line reason, quoted verbatim and linked to its comment. Fix rounds are revisions pushed after review asked for changes. Approved at the first review means every one of Tau Ceti’s review criteria passed on the first try; pull requests not reviewed yet are left out of that count.
• GPU hours are the time the model was working, summed over every attempt, failures included (the time of 2 early attempts were not recorded). Qwen tokens are everything the model read and wrote: 53.8M in all, of which 1.4M written (the tokens of 1 early attempt were not recorded). Most of what it reads is the same files again, served from a cache.
• These are our own measurements, from the records of each run, not estimates. The model runs on the AIs@home network, which today is mostly the maintainer’s own GPUs, some of them rented.
• Pull request states as of 25 Oct 2026. The data is rebuilt once a day and published as JSON: /science/tauceti.json.