TauLib Inspection Bridge

What TauLib Verifies

TauLib is the Lean formalization layer of the program. The active Lean development source remains the public TauLib repository; the Corpus owns a pinned snapshot and generates the public module/declaration browser from that source.

The current projection contains 512 modules and 14607 declarations/evals, pinned to commit cb5e830.

TauLib inside the verification matrix

↓ Download print master · 1536 × 864 JPG · CC BY 4.0

TauLib is one formalization surface inside the broader verification matrix. Lean compilation checks formalized obligations; it does not by itself establish empirical truth.

Release Lines

TauLib is published through two release lines plus a per-result proof-package layer. From an inspection standpoint, each line is a distinct trust-boundary surface:

• TauLib v2 Snapshot

  Citable as a proof basis. Frozen Lean projection of the Second-Edition Corpus; pinned commit and Lean toolchain are stamped in the Release Manifest. Reviewers can clone the pinned commit, re-run lake build, and reproduce the compilation result that this page reports.

• TauLib v3 Library

  Active restructure · not yet citable. Layered library — import-isolated kernel, Mathlib-facing bridges, community-readable module structure — currently in private development. Not a proof basis for any cited Result until it ships publicly; current Results cite the v2 Snapshot.

• Proof Packages

  Per-result · per-package state. Isolated reproducibility bundles for specific formal results. Each package moves through five states: in construction · draft · candidate · released · superseded. Released packages are citable as a per-result proof basis; non-released states should not be cited as proof.

Trust boundary. Lean compilation checks encoded formal obligations. It does not by itself establish empirical truth, bridge adequacy, or external scientific acceptance. The release-line distinction above is about formalization status; the Verification Framework and How to Verify cover the broader inspection questions.

What Verify still owns

Verify does not stop at “the Lean code compiles.” It asks the higher-level inspection questions:

• What does the formalization cover?
• What do the formal terms mean relative to the surrounding Corpus?
• Which bridges connect formal objects to mathematical, physical, biological, or metaphysical claims?
• Which claims remain empirical, semantic, interpretive, or externally assessable?
• Where should a reviewer challenge the assumptions rather than merely re-run compilation?

Inspection routes

• TauLib Browser

  Corpus-native module and declaration pages generated directly from the pinned Lean snapshot.

• Formalization Status

  Current counts, source commit, custom-axiom count, and projection boundary.

• Formal Verification Stack

  How formal proof checking fits into the broader review workflow.

• Verification Framework

  How formal, bridge, empirical, and external-status checks remain distinct.

• Release Manifest

  The pinned public release context and count reconciliation surface.