A visual proof assistant that turns formal reasoning into an interactive node graph — making type theory navigable, intuitive, and collaborative.
Follow development GitHubTraditional theorem provers ask you to write sequential tactic scripts where the logical structure is implicit and the learning curve is steep. The reasoning is there — but it's buried in syntax.
Visual Lean makes the structure explicit. Hypotheses, types, contexts, and dependencies become visible, navigable nodes in a graph. You build proofs by connecting them.
The idea for Visual Lean came from my friend David, who I met in the LSU math department. This is an experimental prototype exploring his concept — built as a side project to see how far the visual inference model can go.
Linear text scripts. Structure is implicit. You read tactics left-to-right and reconstruct the proof tree in your head.
An explicit graph of inference. Contexts, types, and dependencies are visible and navigable. Drag, connect, reason.
Each node is a formal judgment from type theory. Edges capture how hypotheses flow into conclusions.
Strongly typed C++ data model. Four thesis kinds: type declarations, type equivalences, element relations, element equivalences.
C++ compiled to WebAssembly via Emscripten. Dear ImGui + ImNodes for the visual interface. No backend required.
In-memory graph in C++. Zero dependencies. Proving that the inference graph model works.
Persistent state with local PostgreSQL. Save, load, and reuse structured knowledge across sessions.
A shared map of all mathematics. Pull from communal knowledge to build proofs in your own workspace. Contribute back. The platform grows more valuable as more people use it.
Zach — Architecture, WASM/frontend pipeline, product vision
David — Core logic, C++ type theory data structures