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.
TauCeti/, 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.
