Theorem Project
Mankiewicz Extension Theorem
11 approved Cards in the selected reading scope. Follow the dependency-guided reading route and exact source.
Open Project ↗REUSABLE FORMAL MATHEMATICS
MathlibAnnex
Build on Mathlib. Keep the useful mathematics.
MathlibAnnex is a shared library of reusable Lean declarations. Source v0.5.0 is public. Five LFH Projects and 256 unique Card UIDs: the earlier 188-Card edition plus 68 additional GSS UIDs.
Projects and Catalog
Research Companion
Sphere Rigidity
75 approved Cards in the selected reading scope; 467 source declarations in auxiliary exploration. Follow the dependency-guided reading route and exact source.
Open Project ↗Theorem Project
Rosenberg Compact-Operator Model
33 approved Cards in the selected reading scope; 63 source declarations in auxiliary exploration. Follow the dependency-guided reading route and exact source.
Open Project ↗Research Companion
Naimark's problem
68 approved Cards in the main reading scope; CH adds 1 direct Card and reuses 2. Follow the dependency-guided reading route and exact source.
Open Project ↗Research Companion
Geometric Structure Spaces
C*-algebras viewed through Banach-space geometry, using geometric structure spaces to recover spectral information and characterize compact-operator algebras. 69 exact Cards plus reading A as context. One R09 UID is shared with the earlier Catalog; this reading scope adds 68 UIDs.
Open Project ↗Whole-library Catalog
Declaration Card Catalog
256 unique Card UIDs: 188 in the earlier edition plus 69 GSS references, with one shared R09 UID (68 additional). Card identities are shared across Project reading routes.
Browse Catalog ↗Lean for Human (LFH) is the human-readable layer accompanying selected Lean declarations: declaration cards, exact source links, and guided Project views.
Project views organize selected Card routes; full-source declaration exploration remains a separate auxiliary view. A declaration Card belongs to the whole-library Catalog; Project ordering is a reading route, not canonical library order. The earlier 188-Card Catalog brought together: 75 Sphere Rigidity, 11 Mankiewicz, 33 Rosenberg and 69 Naimark Cards. The Naimark Companion contains 68 Cards; the CH consequence is a separate route. Sphere Rigidity includes 75 approved Cards in this published selection. The combined Catalog has 188 earlier + 69 GSS − 1 shared R09 = 256 unique Card UIDs. Reading A is context, not a Card.
One foundation, not a parallel mathematics.
Mathlib is the preferred source of existing results. Project names, paper numbering, and temporary proof scaffolding should not determine the public mathematical API.
When a suitable result becomes available in Mathlib, the preferred provider can move there. The explanations and history should remain connected to the exact declarations they describe.
A declaration, and the mathematics behind it.
The reading unit is a declaration card: an exact Lean statement, an explanation of its assumptions and conclusion, proof steps, citations, and a record of review.
MathlibAnnex declarations and selected Mathlib declarations belong in the long-term catalog. Research-specific material stays in versioned project packs. The generated HTML and PDF are views of those records, not separate versions of the mathematics.
Follow the proof as far as you need.
A reference should lead not only to a theorem name, but to the assumptions and reasoning needed to understand its use. General-purpose cards can be reused; the project explains how a result applies in this proof.
Each declaration card can be read on its own or followed through a Project’s dependency-guided route. Exact source links remain available for readers who want the formal statement and implementation details.
No separate completion of these library projects is required to publish a clearly labelled research briefing.
Return to the researchSource and verification
The canonical source release and the records used to verify it are available separately from the reader-facing Projects and Cards.
Source and release
Current public source release: v0.5.0. The four published LFH Projects and 188 published Card UIDs retain their exact v0.4.0 bindings. The GSS Companion brings the Catalog to 256 unique Card UIDs. R09 retains its exact v0.4.0 source. Existing content terms remain unchanged.