Statistics

How much mathematics has Tau Ceti formalized, and how fast is the roadmap that directs it growing? Each chart plots the total number of lines present at every commit, counted straight from the git history and rebuilt from scratch at each deploy, so the figures cannot drift.

Tau Ceti: lines of Lean by date — The Lean library under `TauCeti/`, total lines by date.

Tau Ceti Roadmap: lines written by date — The human-owned roadmap repository, total lines by date.

The vertical scales differ by an order of magnitude and on purpose: the library is measured in tens of thousands of lines of Lean, the roadmap in thousands of lines of prose and target statements. The library figure counts only the mathematics — the files under TauCeti/ — not the website or tooling.

Which roadmap is all that Lean serving? Every pull request is labelled with the roadmap it advances, so we can split the library by roadmap. The chart below stacks the net lines each roadmap has accrued — every merged PR's additions minus its deletions, attributed to its roadmap — by the day the PR merged. Because it sums diffs rather than counting the lines in the tree, a line later rewritten counts under both PRs, so this measures work landed per roadmap, not a snapshot line count. Infrastructure and refactor PRs, which advance no roadmap, are left out. How far each roadmap has got against its own specification is a different question, answered on the Progress page.

Tau Ceti: cumulative net lines of Lean per roadmap, over time — Net lines added or refactored per roadmap, stacked, by the date each PR merged.

How is the contribution and review pipeline behaving? The first chart separates a PR's total age from the clock on its current state. The author-action clock covers both states that wait on a human, a failed build and a review that requested changes. PRs outside the author-action and review states appear in total time open but not in the two current-state panels. The rolling history uses complete UTC days. The review-cycle chart counts durable label transitions rather than scoreboard comments, because a scoreboard may be edited in place as later rounds complete. A cycle is one entry into review from an author or CI state, so the pipeline swapping awaiting-review for review-in-progress and back within a single round stays one cycle. Its subtitle states when those review-state transitions first appear in project history.

Open pull request age, followed by time awaiting author and time in review — Age of every open PR, then elapsed time in its current author-action or review cycle.

Trailing-seven-day pull request throughput, participation, and merge latency — Merges, active PR authors, and creation-to-merge latency in trailing seven-day UTC windows.

Pull requests reaching each successive review cycle — PRs reaching each review cycle; a cycle begins whenever a PR returns to `awaiting-review` after its author's turn.

Who has taken part? The snapshot below counts GitHub accounts that have opened a pull request or issue, participated in those conversations (including reviews), or authored a commit on the default branch of TauCeti, TauCetiRoadmap, TauCetiWorker, or TauCetiReview. Accounts recognised as automation are dropped: logins carrying GitHub's [bot] suffix, together with the project's own automation aliases. Nothing verifies that the accounts left over belong to people, so any automation the filter does not recognise is still counted. The headline deduplicates accounts across all four repositories; the repository bars deliberately overlap.

Participation across the four Tau Ceti repositories, by repository — Participating accounts by repository, once recognised automation is excluded; an account active in several repositories appears in several bars.

How have merged contributions and reviews accumulated? Like the rolling charts above, these histories are drawn through the last complete UTC day, so a few hours of today never read as a slowdown. They show every contributor while that remains legible, then cap themselves at 24 named lines and combine the remaining long tail. Exact totals for every login, counted right through the snapshot instant, remain available in the generated pr-stats.json. A review is one canonical v1 scoreboard whose posting login also authors a merged PR in the fetched snapshot.

Cumulative merged pull requests by contributor — Cumulative merged PRs by author since project inception.

Cumulative reviews by contributor since project inception. Each review is one canonical v1 scoreboard; edits to an existing scoreboard do not add counts.

Who works where? The two grids below slice the same merges and reviews by area, over the trailing ninety days. Each pull request counts under the arXiv category of the roadmap it carries, as that roadmap declares it in its metadata.toml in TauCetiRoadmap; a roadmap that declares none counts as Unsorted. Between them the grids answer the questions the cumulative histories cannot: who already knows an area well enough to review for it, whether an area is resting on one person, and where somebody has been spending their effort.

The columns are the categories with the most merges in that window, busiest first — every one of those questions is about now. Both grids use the same columns, so they can be read against each other. Past twenty categories the rest would share one Other column, and the quietest contributors are summed into one Other row, so nothing is dropped; exact per-contributor, per-category counts are in pr-stats.json.

Merged pull requests per contributor per arXiv category, over the trailing ninety days — Merged PRs per contributor per arXiv category over the trailing ninety days. Each PR counts under the category of the roadmap it advances.

Reviews per contributor per arXiv category, over the trailing ninety days — Reviews per contributor per arXiv category over the same window and the same columns.