Astrolabe - 3D dependency graph visualizer

Stream: general

[Li, Xinze (Moqian)]

I'll keep posting short videos on my YouTube channel showcasing new Astrolabe features, as well as other tools I'm developing in the future :smiley: : https://www.youtube.com/@xinzzzzz-v7i

[Li, Xinze (Moqian)]

This topic is for anything related to Astrolabe — feature discussions, feedback, ideas, or questions. Feel free to post here! #announce > Astrolabe – 3D Dependency Graph Visualizer for Lean 4

[Alok Singh]

Xinze Li said:

I'll keep posting short videos on my YouTube channel showcasing new Astrolabe features, as well as other tools I'm developing in the future :smiley: : https://www.youtube.com/@xinzzzzz-v7i

Just subscribed :slight_smile:

[Alejandro Radisic]

PR up: Transitive reduction, namespace clustering & density-adaptive edges

Just opened a PR with some graph visualization improvements:

• Transitive reduction - removes redundant edges (A→C when A→B→C exists) for cleaner graphs
• Namespace clustering - nodes in the same Lean namespace (e.g. IChing.Hexagram.*) cluster together
• Density-adaptive springs - hub nodes get longer edges to reduce clutter

Combined with the PR from yesterday about technical nodes, visualizations should be much smoother!

Also fixed node coloring by kind (theorems purple, definitions amber, etc.)

[Li, Xinze (Moqian)]

WOW Thank you!! These are nice features. let me play with these first!

[Li, Xinze (Moqian)]

Quick updates:

1. New PR created: feature/search-panel-and-clustering branch with SearchPanel redesign + improved namespace clustering controls. Set as draft for review before merging.
2. Branch protection enabled: Added ruleset to main branch requiring PR reviews before merge - keeps our collaboration safer.

[Li, Xinze (Moqian)]

@Alejandro Radisic

[Jackie]

Just submitted a PR with the following features:

1. Search Panel Redesign - Redesigned the Search Panel with namespace hierarchy grouping, making it easier to browse and navigate declarations organized by their Lean namespaces.
2. Cluster Separation Control - Added a new parameter to control cluster separation in the 3D force-directed graph, allowing users to adjust how tightly or loosely namespace clusters are grouped together.
3. Improved Force Layout - Increased the sensitivity of cluster separation force for better visual organization of the dependency graph.

[Li, Xinze (Moqian)]

Hi everyone!

Over the past few days, I've received creative contributions to Astrolabe from different people, which are all amazing. This got me thinking — it's not just about building software. It's about exploring how we collaborate as AI breaks down the barriers of software development.

After discussions with people from different backgrounds, I've started assembling an engineering team and written a whitepaper to outline this vision.

I want to be the bridge between inspiration and implementation. With everyone's ideas and creativity, we organize engineers to integrate, and govern through the community.

Website: https://astrolean.io
Repo: https://github.com/Xinze-Li-Bryan/Astrolabe
Whitepaper: https://docs.google.com/document/d/1_PEwX5i0S2YvkueV34L3_FujAZMZQlFs0jGGZNSrpqY/edit
Join our mail list: https://docs.google.com/forms/d/e/1FAIpQLSe5EfHnKQaxNcTpRCUsjVszAmJCcjH7xIOENo6H4ayeW5KgEQ/viewform

Whitepaper is open for editing — feel free to comment.

[Li, Xinze (Moqian)]

Also wondering: would it be better to put the whitepaper on GitHub for PRs, or would people prefer Overleaf?

[Kevin Buzzard]

Can you start a discussion thread in #general (and link to it here) rather than continuing the conversation in #announce ?

[Notification Bot]

5 messages were moved here from #announce > Astrolabe by Johan Commelin.

[Jackie]

(deleted)

[Li, Xinze (Moqian)]

Thanks for help!

Kevin Buzzard said:

Can you start a discussion thread in #general (and link to it here) rather than continuing the conversation in #announce ?

[Li, Xinze (Moqian)]

Hey everyone,

Just created a new release for Astrolabe! :tada:

https://github.com/Xinze-Li-Bryan/Astrolabe/releases/tag/v0.1.9

Could anyone help test if the downloads work on your machine?

• Windows (.exe)
• Linux

Your testing would help all Windows and Linux users. Let me know if you run into any issues!

[Nick Adfor]

Wow, just in few hours there's really an .exe!

[Nick Adfor]

image.png
What is "Click a node on canvas"?

[Nick Adfor]

Well, interesting. It's just I should open the eye:
image.png

[Jackie]

Nick Adfor said:

Well, interesting. It's just I should open the eye:
image.png

Yes, clicking the eye icon shows/hides nodes on the canvas.
The idea is you can build your own custom view of the dependency graph - add the theorems you care about, arrange them spatially however makes sense to you, and save that layout. Useful for focusing on a specific part of a large project or creating a "map" of key results.
This is how a project I tried with Astrolabe looks like after clicking the eye icon
20260120-1713-06.2208864.mp4

[Li, Xinze (Moqian)]

Wow nice！Thanks for helping me reply.

[Nick Adfor]

I've found something. Astrolabe cannot work online so it's not so easy for other people to check the project (because it must work offline and install the whole Lean including Mathlib)

[Jackie]

True, it would be great to have an online version.

[Li, Xinze (Moqian)]

That's a great point! I'm actively looking for an engineering team to build an online version — if we can pull it off, it would make the project much more accessible.

For now, installing Lean is required. After that, you just need to run lake exe cache get (to pull the cached build) followed by lake build. The key is making sure the .ilean files are generated.

[Nick Adfor]

Oh, you need a team! So it might be hard to realize this online page....

[Nick Adfor]

As I've known, leanblueprint just uses Jekyll and html so it does not need to care the problem here such as Astrolabe's movement.

[Nick Adfor]

The problem from my posted picture is just a failure and tiredness after the disaster leanblueprint.

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/blueprint.20only.20shows.20html

[Li, Xinze (Moqian)]

I do have a team in mind — still figuring out the details.

[Kevin Buzzard]

I can recommend Monticone's lean project template which includes leanblueprint and works out of the box. edit: I'm talking about this https://github.com/leanprover-community/LeanProject

[Li, Xinze (Moqian)]

Thanks Kevin! Yeah, Alex actually suggested I work with Pietro on potential integration. We've discussed it — he's been busy but hopefully we can move forward soon.

[Jackie]

Nice to hear that. Makes sense to combine strengths

[Li, Xinze (Moqian)]

(deleted)

[Li, Xinze (Moqian)]

(deleted)

[TyDHC]

If Astrolabe combined with leanblueprint and LeanArchitect, maybe it will be more useful for lean projects

[Li, Xinze (Moqian)]

Open to that! What integration would be most useful for you? @TyDHC