Lean Blueprint
A curated, redacted system map of the Lean-based stack. This dashboard aligns with Lean Blueprint community standards: dependency graphs, status legend, Mathlib anchors, and public evidence without exposing proof scripts or proprietary implementation detail.
Semantic Explorer
Interactive visualizations of the HeytingLean semantic layer. Select a view mode to explore module architecture, semantic relationships, dependencies, or browse individual declarations.
System Map
Module Architecture
Lean Blueprint Dependency Graph
Full dependency graph generated from the Heyting-dev Lean Blueprint toolchain. Click nodes to view details. Drag to pan, scroll to zoom.
Status Matrix
0 public nodesLoading status matrix...
Registries
Loading registries...
Disclosure Levels
Loading disclosure policy...
Lean References
Verified pathways, ontology grounding, and community resources used to validate the public blueprint.
Verified Compilation: Lean to C (Proof-Carrying Pipeline)
A minimal-trust pathway from formal specification to executable artifacts.
Grounding Choice: How Generative Dynamics Replace Axioms
A rule-first approach to emergence and ontology for computation.
Lean Blueprint Dependency Graphs
Directed dependency graphs inspired by community blueprint tooling.
Mathlib Documentation
Public Lean library index and reference material.
Subbooks
Drill into category-specific views, project clusters, and validation-ready packets.
Glossary
Loading glossary...