Astrolabe (Prototype)

This repository is the early prototype of Astrolabe and is no longer actively maintained. The latest version is being developed at factorin-dev/Astrolabe — a new public release is coming soon.

A 3D dependency graph visualization tool for Lean 4 formalization projects. Astrolabe parses your Lean codebase, builds a dependency graph, and renders it in an interactive 3D space.

Features

• 3D force-directed graph visualization with namespace clustering
• Lean 4 .ilean parsing, file watching, sorry detection
• Fuzzy search, namespace browser, dependency explorer
• Monaco editor with Lean 4 syntax highlighting
• Markdown notes with KaTeX math rendering
• 30+ graph analysis algorithms (PageRank, community detection, spectral clustering, Ricci curvature)

Architecture

Next.js + Three.js frontend, Python/FastAPI backend, Tauri (Rust) desktop wrapper.

Quick Start

git clone https://github.com/Xinze-Li-Moqian/Astrolabe.git
cd Astrolabe
npm install
cd backend && pip install -e ".[dev]" && cd ..
npm run dev:all

Collaborating Team

Xinze Li · Alejandro Radisic

License

Apache License 2.0 — see LICENSE for details.