TauLib Formalization Status

Pinned Source

This status page is generated against the Corpus-native TauLib projection, pinned to TauLib commit cb5e830. The active contributor-facing Lean development repo remains GitHub; the Corpus projection owns the pinned browse metadata used by this site.

Current Counts

Metric	Current projection
Modules	512
Declarations / evaluations	14607
Theorems	4857
Definitions	3747
Structures	1518
Examples	371
#eval checks	3923
Custom axioms	3
Registry-linked modules	478
Registry-linked declarations	3998

Reading the registry-linked-vs-total ratio. The "Registry-linked declarations" count is intentionally a subset of "Declarations / evaluations." The unlinked remainder is mostly (a) intermediate lemmas — small helper results used inside larger proofs that the Corpus does not assign individual registry IDs to, (b) namespace and structure-projection declarations (instance / private def / `protected`) generated as scaffolding around the registered theorems, and (c) low-level type-class inference machinery and small `rfl`-form computations that are kernel-honest but not Corpus-tracked. Registry-tracked declarations are the named surface a reviewer would cite; the unlinked declarations are the proof-internal machinery that lets the registered ones close. The ratio therefore reads as "this many of our internal Lean declarations have been promoted to named Corpus objects with stable IDs," not "only this many of our declarations are real." Future waves will widen registry coverage; a 100% ratio is not a target — a stable named surface for reviewer use is the actual goal.

Verification Boundary

TauLib verifies Lean-formalized statements and executable checks. It does not, by itself, verify empirical adequacy, semantic correspondence to manuscript prose, bridge sufficiency, life-recovery interpretation, or external acceptance. Those layers are inspected through the broader Verify matrix.

Build Context

Lean toolchain: v4.28.0-rc1
Mathlib revision: 85028a6
Source license: Apache-2.0
Public source repo: Panta-Rhei-Research/taulib

For release-level count reconciliation and trusted-base framing, use the Release Manifest.

TauLib Formalization Status

Pinned Source

Current Counts

Verification Boundary

Build Context

Save or share this page for inspection

Quick access

Common starting points

Site help