TauLib Technical Overview
Canonical v1.0 technical overview of TauLib as the Lean 4 formalization layer and Verify/TauLib inspection route.
Canonical Artifact
TauLib Technical Overview (WP003) is the canonical technical white paper for the TauLib Lean 4 formalization layer. It explains what TauLib is, how its architecture is inspected, what the current Release Manifest pins, and how the Verify lane exposes the trust budget around the release.
The Technical Overview is deliberately narrower than the τ-Theory Executive Synopsis (WP002). It does not restate the whole theory construction. It routes technically minded readers into the formalization surface: repository, generated docs, release manifest, no-sorry check, custom axiom inventory, TCB disclosure, Registry correspondence, and review workflow.
Release Metadata
| ID | wp003 |
|---|---|
| Status | Canonical v1.0 |
| Release date | 2026-05-12 |
| Short route | https://prrp.site/wp003 |
| Mnemonic route | https://prrp.site/wp-taulib |
| Canonical route | /publications/anchor-documents/wp003-taulib-technical-overview/ |
| /assets/pdfs/anchor-documents/wp003-taulib-technical-overview.pdf | |
| Pages | 39 |
| Size | 304008 bytes |
| SHA-256 | e6a1f6bced734b6ad5679f8a1793eabd59e013bf6c0631523f427887544a8a9d |
| License | CC-BY-4.0 |
Current Release Snapshot
The May 2026 release snapshot summarized in the Technical Overview is pinned by the TauLib Release Manifest:
| Lean toolchain | v4.28.0-rc1 |
|---|---|
| Mathlib snapshot | 85028a6 |
| TauLib snapshot | cb5e830 |
| Modules/files | 512 |
| Lean source lines | 142,406 |
| Theorem/lemma records | 4,863 |
| Declarations and eval records | 14,601 |
| Custom axioms | 3 |
| Sorry count | 0 |
Claim Boundary
The Technical Overview documents the represented formalization release and its inspection routes. It does not claim empirical validation, semantic adequacy, complete formal coverage of the research program, peer-review completion, external acceptance, deployment readiness, product availability, policy adoption, or achieved impact.
Hashes attest to the PDF bytes only; they do not certify correctness, peer review, empirical adequacy, legal status, DOI registration, or content validity.
Inspection Routes
- Formalization overview: TauLib
- Audit surface: Verify/TauLib
- Pinned release facts: Release Manifest
- Trust-budget disclosure: Custom Axioms and TCB
- Source repository: Panta-Rhei-Research/taulib
- Generated documentation: taulib.site
Citation
Fuchs, Thorsten and Anna-Sophie Fuchs. “TauLib Technical Overview.” White Paper wp003, Panta Rhei Research Program, canonical v1.0 release, May 2026.
Save or share this page for inspection
Download a portable dossier, copy a reviewer note, or send this page to someone who can inspect it.