THE RESEARCH ATLAS VOL. 04 / TWO LANGUAGES
Mathematical ideas.
Formal connections.
From a statement on the page to a declaration in Lean. Explore two sides of the same mathematical landscape, connected by the references in each project’s blueprint.
Connecting the mathematical landscape…
Loading statements, declarations, and their blueprint connections.
Circles are informal statements and proofs; squares are Lean declarations. Cross-links connect the two sides. Colors group projects. Enable “Show dependencies” to explore informal references and proof links within the left side; arrows follow the source’s direction. Formal-to-formal dependencies are not included in this dataset. Entries without a resolved counterpart remain visible. Unresolved references appear as hollow squares and dashed lines when enabled. Data, coverage & provenance ↗