Introduction

Astrolabe is a 3D dependency graph visualization tool for Lean 4 formalization projects.

Astrolabe is an intelligent dependency graph visualization tool designed specifically for Lean 4 projects. It transforms complex proof dependencies into interactive 3D visualizations, helping mathematicians, developers, and researchers understand and navigate formalized mathematics.

What is Astrolabe?

Astrolabe provides a visual exploration environment for Lean 4 codebases. It automatically parses your project structure, builds a dependency graph, and renders it in an interactive 3D space where you can:

• Explore theorem dependencies visually
• Search and navigate through namespaces
• Analyze graph metrics (PageRank, centrality, clustering)
• Edit code with integrated Monaco editor
• Take notes with Markdown and KaTeX support

Key Features

• 3D Visualization: Force-directed graph layout with physics simulation, namespace clustering, and smooth camera controls
• Lean 4 Integration: Automatic parsing, file watching, sorry detection, and declaration type recognition
• Search & Navigation: Fuzzy search, namespace browser, dependency explorer, and lens picker (Cmd+K)
• Canvas Management: Focus subgraphs, virtual nodes, position persistence, and undo/redo support
• Code Editing: Monaco editor with Lean 4 syntax highlighting, Markdown notes with KaTeX math rendering
• Advanced Analysis: 30+ graph theory algorithms including PageRank, community detection, spectral clustering, and Ricci curvature

Architecture

Astrolabe consists of three main components:

Getting Started

Ready to visualize your Lean project? Check out our Getting Started guide to install and run Astrolabe.

Community

Astrolabe is open source and community-driven. You can earn ASTRO Points by contributing code, reporting issues, or creating content. See our Contribute page for details.