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.4.0 is public. Four Projects connect to a whole-library Catalog of 188 Declaration Cards.
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 ↗Whole-library Catalog
Declaration Card Catalog
188 approved Cards across MathlibAnnex, sharing identities 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. This Catalog brings together 188 Cards: 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.
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
Source v0.4.0 is public. The whole-library Catalog presents 188 Cards across four Project reading routes. Existing content terms remain unchanged.