User-guide

# Navigating a Blueprint Site This guide explains how to browse and use a Side-by-Side Blueprint site. ## Dashboard The dashboard is the homepage of every blueprint site. It provides a quick overview of your formalization project through four panels: - **Stats** -- Shows how many declarations are in each status category (not ready, proven, fully proven, etc.) with a completion percentage. This tells you at a glance how much work remains. - **Key Theorems** -- Lists the most important declarations in the project, marked by the author. Each entry shows a colored status dot indicating its current state. - **Messages** -- Notes from the project author about specific declarations, such as progress updates or context. - **Project Notes** -- Organized into sections for blocked items, potential issues, technical debt, and miscellaneous notes. Useful for understanding what needs attention. ## Dependency Graph The dependency graph page shows how all theorems, lemmas, and definitions relate to each other. ### Reading the Graph - **Node shapes**: Rectangles represent definitions, structures, and classes. Ellipses represent theorems, lemmas, and propositions. - **Node colors**: Each node is colored by its formalization status. See [Status Colors Explained](status-colors.md) for details. - **Solid lines**: The target declaration is used in the proof of the source. - **Dashed lines**: The target declaration is used in the statement (type signature) of the source. - **Direction**: Arrows point from dependencies to dependents (bottom to top in the hierarchy). ### Interacting with the Graph - **Zoom**: Scroll the mouse wheel to zoom in and out, centered on your cursor position. - **Pan**: Click and drag to move around the graph. - **Fit to Window**: Use the fit-to-window button in the toolbar to reset the view so the entire graph is visible. - **Click a node**: Opens a modal with the full declaration details, including the LaTeX statement, Lean code, status, and links. ### Graph Warnings The graph page may display validation warnings: - **Disconnected components** -- Some declarations are not connected to the rest of the graph. This could indicate missing dependencies or orphaned declarations. The Tao incident showed that disconnected final theorems can mean proofs are proving the wrong thing. - **Cycles detected** -- Circular dependencies exist in the graph, which may indicate a logical issue. ## Chapter Pages Chapter pages are the core of a blueprint site. They display mathematical content organized by the LaTeX document structure. ### Side-by-Side Display Each declaration appears as a side-by-side panel: - **Left side**: The LaTeX mathematical statement, rendered with MathJax. - **Right side**: The corresponding Lean 4 code with syntax highlighting. - **Status dot**: A colored dot in the header indicates the formalization status. ### Proof Toggle Proofs can be expanded or collapsed: - Click the proof header area to toggle visibility. - When a LaTeX proof section is expanded, the corresponding Lean proof code expands simultaneously (and vice versa). - This synchronization helps you compare the informal and formal proofs step by step. ### Hover Information Hover over identifiers in the Lean code to see: - **Type signatures**: The full type of a function, theorem, or variable. - **Documentation**: Any doc strings attached to the declaration. - **Tactic state**: In proof blocks, hovering shows the current proof goal at that point. ### Rainbow Brackets Nested brackets in Lean code are colored with cycling colors to help you match opening and closing brackets visually. This applies to parentheses `()`, square brackets `[]`, and curly braces `{}`. ## Paper If the project includes a paper, you can view it through the Paper link in the sidebar. - **Paper [TeX]**: An HTML rendering of the academic paper, styled similarly to ar5iv.org. - **PDF [TeX]**: An embedded PDF viewer for the compiled paper. Declarations in the paper include **verification badges** showing the formalization status, with links back to the corresponding blueprint page. ## Theme Toggle Use the theme toggle switch in the sidebar to switch between light mode and dark mode. Your preference is saved in your browser and persists across visits. ## Sidebar Navigation The sidebar provides navigation to all parts of the site: - **Dashboard**: Returns to the homepage overview. - **Dependency Graph**: Opens the interactive graph view. - **Blueprint chapters**: Expand the Blueprint section to see all chapters and sections. Click any chapter or section to navigate to it. The current page is highlighted. - **Paper / PDF**: Links to the paper view (if available). - **GitHub**: Links to the project source code. - **API Docs**: Links to DocGen4 documentation (if configured). On chapter pages, the chapter list in the sidebar automatically expands to show where you are in the document.