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.
Two concrete starting points.
Mankiewicz Theorem Project
A derived proof route through the eleven public canonical Declaration Cards, with prerequisites, used-by navigation, exact source and a three-page PDF.
Open the ProjectSphere Rigidity Research Companion
A progressive Research Companion with 467 exact declaration nodes and zero public Cards.
Open the CompanionNo separate completion of these library projects is required to publish a clearly labelled research briefing.
Return to the research