Panta Rhei — Formalization
Transitional Archival Surface — Superseded
This repository is retained as a transitional archival surface.
The authoritative live Lean 4 formalization of the Panta Rhei kernel now lives in taulib.
The frozen edition-bound snapshot used for the Second Edition lives in books.
The formalization repository served as the frozen verification archive for the Panta Rhei book series during the 2nd Edition publication process (March 2026). It contained the exact Lean 4 codebase referenced in the published books.
With the research program's maturation, the formalization architecture has been clarified:
- Live, evolving formalization →
taulib(450 modules, 125,771 lines, 4,332 theorems, 0 sorry in Books I–VI) - Frozen edition-bound snapshot →
books(exact commit/tag the 2nd Edition is based on) - This repo → transitional archive, retained for link stability
| If you want to... | Go to... |
|---|---|
| Explore the live formalization | taulib |
| Verify the exact 2nd Edition claims | books |
| Read the TauLib documentation | panta-rhei.site/verify/taulib/ |
| Browse the research website | panta-rhei.site |
This repository is archived. No new commits will be made. Issues and PRs are closed.
For questions about the formalization, please use the TauLib repository or contact the research program.