Tengoku

Every theorem in Tengoku is one line in a data file in the public Tengoku repository. We count those lines. Nobody types the numbers in.

• Leak-trusted: theorems Leak has checked from scratch, plus the theorems in libraries that were added whole.
• Tentative: theorems with a real proof in their original source that Leak has not checked yet.
• The total is both added together, counting each theorem once: a tentative record of a theorem that is already Leak-trusted (its library was added whole after it was harvested, or the record was promoted) is not counted again. Today's number is recounted about every ten minutes.

The graph adds one point a day and starts on 10 Sep, the day the repository was created. Days before daily logging began were rebuilt from the repository's history using the same rule, so they are exact for those days. Moving theorems between files or folders does not change a count, because we count theorems, not files.

Yield is, for each library, how much of its own theorems were kept: the share of its own theorems and lemmas that are Leak-trusted in Tengoku. The library's total is counted from its source code at the version Tengoku pins, with the same scanner Tengoku uses to read it. Tentative theorems do not count towards yield, because Leak has not checked them yet. Libraries with no pinned source (slices of Mathlib, sets written by AI) show a dash.