diff --git a/.github/workflows/readme-stats.yml b/.github/workflows/readme-stats.yml
new file mode 100644
index 0000000000..6734c37f92
--- /dev/null
+++ b/.github/workflows/readme-stats.yml
@@ -0,0 +1,49 @@
+name: README stats
+
+on:
+ push:
+ branches:
+ - main
+ # Only the inputs to the stats can change them. The refresh commit
+ # below touches README.md only, which is NOT in this list, so it
+ # cannot re-trigger this workflow (no commit loop).
+ paths:
+ - 'LeanPool/**'
+ - 'python/lean_pool/stats.py'
+ - '.github/workflows/readme-stats.yml'
+ workflow_dispatch:
+
+concurrency:
+ group: ${{ github.workflow }}-${{ github.ref }}
+ cancel-in-progress: true
+
+permissions:
+ contents: write
+
+jobs:
+ refresh:
+ runs-on: ubuntu-latest
+ steps:
+ - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+
+ - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+ with:
+ enable-cache: true
+
+ - name: Install dependencies
+ run: cd python && uv sync --locked
+
+ - name: Refresh README stats
+ run: cd python && uv run python -m lean_pool.stats --repo ..
+
+ - name: Commit if changed
+ run: |
+ if git diff --quiet -- README.md; then
+ echo "README stats already up to date."
+ exit 0
+ fi
+ git config user.name "github-actions[bot]"
+ git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
+ git add README.md
+ git commit -m "chore: refresh README stats [skip ci]"
+ git push
diff --git a/README.md b/README.md
index 03946bdbc2..efc0d0b7fd 100644
--- a/README.md
+++ b/README.md
@@ -11,6 +11,12 @@
Lean Pool sits between [`mathlib`](https://github.com/leanprover-community/mathlib4) and [`merely-true`](https://github.com/merely-true/merely-true), preserving Lean 4 formalizations that don't fit mathlib's scope. Instead of mathlib's high-bar human review, it relies on deterministic linters and LLM judgment, so it can grow faster while staying `sorry`-free and pinned to the latest Mathlib. See [`MOTIVATION.md`](MOTIVATION.md) for the why, and browse the API docs at .
+
+**90** formalization projects · **676,138** lines of Lean
+
+
+(stats above are refreshed automatically by [`readme-stats.yml`](.github/workflows/readme-stats.yml) — edit [`python/lean_pool/stats.py`](python/lean_pool/stats.py), not the numbers)
+
So far, projects have been added by hand: each is a suitable, permissively licensed (Apache-2.0 or MIT) Lean repository, bumped to the latest Lean and Mathlib, made to pass [CI](.github/workflows/lean_action_ci.yml) — it builds warning-free and clears Mathlib's linters, the style checker, and the repository quality gates (no `sorry`/`admit`, no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, no `unsafe`/`partial`, file headers, size limits) — and an [LLM review](.github/REVIEW_RULES.md) of fit and significance, then merged.
### Getting started
diff --git a/python/lean_pool/stats.py b/python/lean_pool/stats.py
new file mode 100644
index 0000000000..5e3f01ccef
--- /dev/null
+++ b/python/lean_pool/stats.py
@@ -0,0 +1,176 @@
+"""Compute headline repository statistics and write them into the README.
+
+The main ``README.md`` carries a short, machine-maintained line reporting
+how many projects live in the pool and how many lines of Lean they total.
+This module derives both numbers from the single sources of truth
+(``LeanPool/projects.yml`` for the project count, the ``LeanPool/`` tree
+for the line count) and rewrites the block delimited by two HTML comment
+markers:
+
+
+ ...generated line goes here...
+
+
+Run ``python -m lean_pool.stats --repo .`` to rewrite the block, or pass
+``--check`` to fail without writing when the block is stale (used by CI to
+decide whether a refresh commit is needed).
+"""
+
+from __future__ import annotations
+
+import argparse
+import re
+import sys
+from dataclasses import dataclass
+from pathlib import Path
+
+import yaml
+
+BEGIN_MARKER = ""
+END_MARKER = ""
+
+_MARKER_BLOCK = re.compile(
+ re.escape(BEGIN_MARKER) + r".*?" + re.escape(END_MARKER),
+ re.DOTALL,
+)
+
+# Directories whose ``.lean`` files are build artefacts or vendored
+# dependencies rather than pooled project source. ``LeanPool/`` should
+# never contain these, but excluding them keeps the count honest if a
+# stray build tree ever lands under it.
+_LOC_EXCLUDE_DIR_NAMES = frozenset({".lake", ".git", "lake-packages", "build"})
+
+
+@dataclass(frozen=True)
+class Stats:
+ """Headline counts shown in the README."""
+
+ projects: int
+ lines_of_lean: int
+
+
+def count_projects(projects_yml_path: Path) -> int:
+ """Return the number of projects registered in ``projects.yml``.
+
+ Args:
+ projects_yml_path: Path to ``LeanPool/projects.yml``.
+
+ Returns:
+ The length of the top-level ``projects`` list, or ``0`` if the
+ file is missing, malformed, or has no ``projects`` key.
+ """
+ if not projects_yml_path.is_file():
+ return 0
+ data = yaml.safe_load(projects_yml_path.read_text()) or {}
+ if not isinstance(data, dict):
+ return 0
+ projects = data.get("projects") or []
+ if not isinstance(projects, list):
+ return 0
+ return len(projects)
+
+
+def count_lean_loc(pool_dir: Path) -> int:
+ """Sum lines across every ``.lean`` file under the pool tree.
+
+ Walks ``pool_dir`` recursively and totals lines across all files
+ matching ``*.lean``, skipping build/dependency directories. Line
+ counting uses raw newline semantics so it matches ``wc -l``.
+
+ Args:
+ pool_dir: Path to the ``LeanPool/`` directory.
+
+ Returns:
+ The total line count, or ``0`` if the directory is missing.
+ """
+ if not pool_dir.is_dir():
+ return 0
+ total = 0
+ for path in pool_dir.rglob("*.lean"):
+ if any(part in _LOC_EXCLUDE_DIR_NAMES for part in path.parts):
+ continue
+ try:
+ with path.open("rb") as handle:
+ total += sum(1 for _ in handle)
+ except OSError:
+ continue
+ return total
+
+
+def collect_stats(root: Path) -> Stats:
+ """Gather all README statistics for the checkout at ``root``."""
+ return Stats(
+ projects=count_projects(root / "LeanPool" / "projects.yml"),
+ lines_of_lean=count_lean_loc(root / "LeanPool"),
+ )
+
+
+def render_stats(stats: Stats) -> str:
+ """Render the stats block body (without the surrounding markers)."""
+ return (
+ f"**{stats.projects}** formalization projects · "
+ f"**{stats.lines_of_lean:,}** lines of Lean"
+ )
+
+
+def apply_stats(readme_text: str, stats: Stats) -> str:
+ """Return ``readme_text`` with the stats block replaced.
+
+ Raises:
+ ValueError: If the BEGIN/END markers are not present.
+ """
+ if not _MARKER_BLOCK.search(readme_text):
+ raise ValueError(
+ f"Could not find stats markers in README. "
+ f"Expected '{BEGIN_MARKER}' ... '{END_MARKER}'."
+ )
+ replacement = f"{BEGIN_MARKER}\n{render_stats(stats)}\n{END_MARKER}"
+ return _MARKER_BLOCK.sub(replacement, readme_text, count=1)
+
+
+def _parse_args(argv: list[str]) -> argparse.Namespace:
+ parser = argparse.ArgumentParser(description=__doc__)
+ parser.add_argument(
+ "--repo",
+ type=Path,
+ default=Path(__file__).resolve().parents[2],
+ help="Repository root. Defaults to the checkout containing this package.",
+ )
+ parser.add_argument(
+ "--check",
+ action="store_true",
+ help="Exit non-zero if the README stats block is stale; do not write.",
+ )
+ return parser.parse_args(argv)
+
+
+def main(argv: list[str] | None = None) -> int:
+ """Run the stats CLI."""
+ args = _parse_args(sys.argv[1:] if argv is None else argv)
+ root = args.repo.resolve()
+ readme_path = root / "README.md"
+ original = readme_path.read_text()
+ stats = collect_stats(root)
+ updated = apply_stats(original, stats)
+
+ if args.check:
+ if updated != original:
+ print(
+ "README stats are out of date. Run "
+ "`uv run python -m lean_pool.stats --repo .` and commit.",
+ file=sys.stderr,
+ )
+ return 1
+ print("README stats are up to date.")
+ return 0
+
+ if updated != original:
+ readme_path.write_text(updated)
+ print(f"Updated README stats: {render_stats(stats)}")
+ else:
+ print("README stats already up to date.")
+ return 0
+
+
+if __name__ == "__main__":
+ raise SystemExit(main())
diff --git a/python/tests/test_stats.py b/python/tests/test_stats.py
new file mode 100644
index 0000000000..555c8bed68
--- /dev/null
+++ b/python/tests/test_stats.py
@@ -0,0 +1,104 @@
+"""Tests for README statistics generation."""
+
+from __future__ import annotations
+
+from pathlib import Path
+
+import pytest
+
+from lean_pool.stats import (
+ Stats,
+ apply_stats,
+ collect_stats,
+ count_lean_loc,
+ count_projects,
+ main,
+ render_stats,
+)
+
+PROJECTS_YML = """projects:
+ - slug: alpha
+ title: Alpha
+ - slug: beta
+ title: Beta
+"""
+
+
+def _write_pool(root: Path) -> None:
+ """Create a minimal LeanPool tree with two projects and known LOC."""
+ pool = root / "LeanPool"
+ pool.mkdir()
+ (pool / "projects.yml").write_text(PROJECTS_YML)
+ (pool / "Alpha.lean").write_text("line1\nline2\nline3\n")
+ nested = pool / "Beta"
+ nested.mkdir()
+ (nested / "Core.lean").write_text("only-one-line\n")
+
+
+def test_count_projects(tmp_path: Path) -> None:
+ """The project count is the length of the projects list."""
+ _write_pool(tmp_path)
+ assert count_projects(tmp_path / "LeanPool" / "projects.yml") == 2
+
+
+def test_count_projects_missing_file(tmp_path: Path) -> None:
+ """A missing registry yields zero rather than raising."""
+ assert count_projects(tmp_path / "nope.yml") == 0
+
+
+def test_count_lean_loc(tmp_path: Path) -> None:
+ """Lines are summed recursively across every .lean file."""
+ _write_pool(tmp_path)
+ assert count_lean_loc(tmp_path / "LeanPool") == 4
+
+
+def test_count_lean_loc_skips_build_dirs(tmp_path: Path) -> None:
+ """Build/dependency directories are excluded from the count."""
+ _write_pool(tmp_path)
+ artefact = tmp_path / "LeanPool" / ".lake" / "Dep.lean"
+ artefact.parent.mkdir()
+ artefact.write_text("a\nb\nc\nd\ne\n")
+ assert count_lean_loc(tmp_path / "LeanPool") == 4
+
+
+def test_collect_stats(tmp_path: Path) -> None:
+ """Both headline numbers are gathered from the checkout."""
+ _write_pool(tmp_path)
+ assert collect_stats(tmp_path) == Stats(projects=2, lines_of_lean=4)
+
+
+def test_apply_stats_replaces_block() -> None:
+ """Only the marked block is rewritten; surrounding text is kept."""
+ readme = "intro\n\nold\n\noutro\n"
+ updated = apply_stats(readme, Stats(projects=2, lines_of_lean=4))
+ assert render_stats(Stats(projects=2, lines_of_lean=4)) in updated
+ assert "old" not in updated
+ assert updated.startswith("intro\n")
+ assert updated.endswith("outro\n")
+
+
+def test_apply_stats_requires_markers() -> None:
+ """A README without the markers is a hard error."""
+ with pytest.raises(ValueError, match="stats markers"):
+ apply_stats("no markers here", Stats(projects=1, lines_of_lean=1))
+
+
+def test_main_writes_and_is_idempotent(tmp_path: Path) -> None:
+ """Writing fills the block, and re-running changes nothing."""
+ _write_pool(tmp_path)
+ readme = tmp_path / "README.md"
+ readme.write_text("\n\n\n")
+
+ assert main(["--repo", str(tmp_path)]) == 0
+ assert "**2** formalization projects" in readme.read_text()
+ # A second write is a no-op, and --check now passes.
+ assert main(["--repo", str(tmp_path)]) == 0
+ assert main(["--repo", str(tmp_path), "--check"]) == 0
+
+
+def test_main_check_fails_when_stale(tmp_path: Path) -> None:
+ """`--check` exits non-zero when the block is out of date."""
+ _write_pool(tmp_path)
+ readme = tmp_path / "README.md"
+ readme.write_text("\nstale\n\n")
+ assert main(["--repo", str(tmp_path), "--check"]) == 1