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 Theorem Project view of the Mankiewicz Extension Theorem, bound to MathlibAnnex v0.2.0. Eleven declaration explanations have completed source–exposition correspondence review; public Card links are not yet active.
Open the Project viewSphere Rigidity Research Companion
A progressive Research Companion for Sphere Rigidity with 467 exact declaration nodes, route summaries and source links. Cards remain in preparation.
Open the CompanionNo separate completion of these library projects is required to publish a clearly labelled research briefing.
Return to the research