Statistics

How much physics has EpsilonEridani 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.

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 EpsilonEridani/ — 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.

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.

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 EpsilonEridani, EpsilonEridaniRoadmaps, EpsilonEridaniWorker, or EpsilonEridaniReview. 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.

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.

Who works where? The two grids below slice the same merges and reviews by the roadmap each PR carries, over the trailing ninety days. Between them they answer the questions the cumulative histories cannot: who already knows an area well enough to review for it, whether a roadmap is resting on one person, and where somebody has been spending their effort.

The columns are the fifteen roadmaps with the most merges in that window, rather than the largest of all time — every one of those questions is about now, and a whole-history cut would hold a column for a roadmap that finished in July while an active one could not get in. Both grids use the same columns, so they can be read against each other. Everything past the cut is summed into one Other column and the quietest contributors into one Other row, so nothing is dropped; exact per-contributor, per-roadmap counts are in pr-stats.json.