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.

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? Unlike the rolling charts above, these histories include the current partial UTC day through the snapshot time. 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 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.