Vislean

Vislean allows users to manipulate mathematical equations directly on a computer by simply dragging and dropping.

Features

• Intuitively manipulate equations by dragging and dropping, including commutativity, distributivity, factorizing, smart merging of terms, cancelling fractions and more.
• Manage multiple equations at the same time; solve simultaneous equations.
• Apply theorems and prove trigonometric identities.
• Thorough tutorial explaining how to use the software, accessible to people without mathematical backgrounds.

Installation

Unfortunately, Vislean can only be installed on Linux machines.

1. Install Python (uv is recommended but optional)
2. Install Lean
3. Fork the repo and run the installation script

git clone https://github.com/FergusMunro/Vislean
cd Vislean
./runVislean.sh

Implementation

Vislean is implemented by interacting with Lean using PyPantograph. Each expression is delaborated into Syntax which is then formatted into JSON, via a meta-programmed tactic. This is converted into an AST in Python and certain expressions are parsed specially (for example, nested multiplication is flattened into a single tree node to make commutative swaps easier). This is then rendered in a Qt QGraphicsScene and certain actions generate certain tactics that are fed back to Lean.

Gallery

A simple equation. An equation containing a double bracket.

simplecropped.mp4

simultaneouscropped.mp4

trigcropped.mp4