Theorem relational dependencies automatic extraction and visualization as a graph for Lean4.

Related tags

Graphics lean-graph
Overview

Lean Graph

Interactive visualization of dependencies for any theorem/definitions in your Lean project.

Fermat last theorem four

How to use

In your browser: lean-graph.com

Or run locally

  1. Copy the DependencyExtractor.lean into your project folder (either from GitHub, or download it in the web app)
  2. In the top of the file import the files where are the theorems/definitions you want to extract the graph for
  3. In the bottom of the file there is an #eval line where you can specify your own custom theorem/definition name
  4. Uncomment that same line to get the .json file
  5. Run the Rust project using cargo run --release or cargo r and select your .json file

What's next

Visualization improvements

As it is now, it is hard to visualize large theorems without getting lost, improvement of the force graph algorithm but more importantly the coloring and visualization of individual nodes are needed. Ideal case:

  • Related theorems and lemmas should be clustered together and have shades of similar colors
  • More relevant / larger definitions should be more visible and easier to find
  • After selecting a node, user should be able to see more specifically what that node depends on

Additional features

  • Sharing of visualizations
  • After clicking on node, allow for seeing the documentation
  • Lazy loading of depending nodes
  • Option to visualize any Mathlib constant, without the need of running script locally

If you want to see these features, any contribution is welcome.

You might also like...
Rust library for of graph ensembles

Rust library for random graph ensembles Minimal Rust version: 1.55.0 Implements simple sampling and monte carlo (or rather markov-) steps, that can be

A Graph implemented using nothing but `Vec`s in rust

VecGraph A Graph implemented using nothing but Vecs in rust. Details The graph is implemented using two Vecs: nodes and edges. nodes stores "nodes". w

Simple, performant graph generator for Feynman diagrams* ⚛️
Simple, performant graph generator for Feynman diagrams* ⚛️

Feynman diagram generator ⚛️ A simple generator of "Feynman diagram" permutations (as defined by problem 781). Incrementally builds isomorphically uni

CLI for image processing with histograms, binary treshold and other functions

Image-Processing-CLI-in-Rust CLI for processing images in Rust. Some implementation is custom and for some functionality it uses 3rd party libraries.

GLFW3 bindings and idiomatic wrapper for Rust.

glfw-rs GLFW bindings and wrapper for The Rust Programming Language. Example extern crate glfw; use glfw::{Action, Context, Key}; fn main() { le

Safe and rich Rust wrapper around the Vulkan API
Safe and rich Rust wrapper around the Vulkan API

Vulkano See also vulkano.rs. Vulkano is a Rust wrapper around the Vulkan graphics API. It follows the Rust philosophy, which is that as long as you do

A cool, fast maze generator and solver written in Rust
A cool, fast maze generator and solver written in Rust

MazeCruncher Welcome to maze cruncher! Download Standalone Here Usage To get started, just run the standalone .exe in target/release or compile and ru

A high-performance SVG renderer, powered by Rust based resvg and napi-rs.
A high-performance SVG renderer, powered by Rust based resvg and napi-rs.

resvg-js resvg-js is a high-performance SVG renderer, powered by Rust based resvg and napi-rs. Fast, safe and zero dependencies! No need for node-gyp

Sub-pixel precision light spot rendering library for astronomy and video tracking applications.

Planetarium Sub-pixel precision light spot rendering library for astronomy and video tracking applications. Example usage use planetarium::{Canvas, Sp

Owner
Patrik Číhal
Patrik Číhal
Real-time 3D orientation visualization of a BNO055 IMU using Bissel and Bevy

orientation This is a demonstration of real-time visualization of the attitude of a BNO055 IMU across a wireless network to a Bevy app using the Bisse

chris m 4 Dec 10, 2022
3D Solar System visualization

Description This project is an unrealistic 3D Solar System visualization. It was made for Computer graphics course, that I took at the University of W

Michał Sala 1 Feb 22, 2022
A simple and elegant, pipewire graph editor

pw-viz A simple and elegant, pipewire graph editor This is still a WIP, node layouting is kinda jank at the moment. Installation A compiled binary is

null 180 Dec 27, 2022
GraphScope: A One-Stop Large-Scale Graph Computing System from Alibaba

A One-Stop Large-Scale Graph Computing System from Alibaba GraphScope is a unified distributed graph computing platform that provides a one-stop envir

Alibaba 2.2k Jan 1, 2023
Graph data structure library for Rust.

petgraph Graph data structure library. Supports Rust 1.41 and later. Please read the API documentation here Crate feature flags: graphmap (default) en

null 2k Jan 9, 2023
A graph library for Rust.

Gamma A graph library for Rust. Gamma provides primitives and traversals for working with graphs. It is based on ideas presented in A Minimal Graph AP

Metamolecular, LLC 122 Dec 29, 2022
Simple but powerful graph library for Rust

Graphlib Graphlib is a simple and powerful Rust graph library. This library attempts to provide a generic api for building, mutating and iterating ove

Purple Protocol 177 Nov 22, 2022
🦀 Rust Graph Routing runtime for Apollo Federation 🚀

Apollo Router The Apollo Router is a configurable, high-performance graph router for a federated graph. Getting started Follow the quickstart tutorial

Apollo GraphQL 502 Jan 8, 2023
A graph crate with simplicity in mind

A graph crate with simplicity in mind. Prepona aims to be simple to use (for users of the crate) and develop further (for contributors). Nearly every

Mohamad Amin Rayej 80 Dec 15, 2022
Graph API client writen in Rust

graph-rs Now available on stable Rust at crates.io graph-rs-sdk = "0.1.0" 0.1.0 and above use stable Rust. Anything before 0.1.0 uses nightly Rust. M

Sean Reeise 56 Jan 3, 2023