Lean Experiment is a small lab for exploring Lean tooling UX. It ships a proof walkthrough generator (LLM-backed), an interactive Mathlib treemap, and reference/visualization pages that experiment with how proof state can be taught and inspected.
- Proof walkthrough generator: paste a Lean proof and get a step-by-step explanation from an LLM.
- Mathlib treemap: D3 visualization of Mathlib file metrics, with local folder scanning support in the Tauri app.
- Tactic reference: quick lookup table of common Lean tactics and examples.
- Visualizer scaffold: mock UI for goal-state graphs, tactic timelines, and dependency views.
The treemap accepts both the simple entries / tree JSON schemas and richer
metrics reports (including JBlow-style metrics, module/file borders, and blend weights).
src/App.tsx: main proof walkthrough UI.src/pages/MathlibPage.tsx: treemap visualization and Mathlib scanner.src/pages/TacticsPage.tsx: tactic reference page.src/pages/VisualizerPage.tsx: proof-state visualizer scaffold.api/: Vercel serverless endpoints, including/api/explainand Lean session proxy stubs.
- Node.js + npm
OPENAI_API_KEYfor/api/explain(used by the walkthrough generator)
Run the dev server:
npm run devBuild for production:
npm run buildBuild the webview bundle and copy it into the extension:
npm run build
node vscode-extension/scripts/copy-webview.jsCompile the extension:
cd vscode-extension
npm install
npm run compileIn VS Code, run the command Lean Experiment: Open Mathlib Treemap.
Ubuntu 24.04 dependencies (from the Tauri docs):
sudo apt update
sudo apt install libwebkit2gtk-4.1-dev \
build-essential \
curl \
wget \
file \
libxdo-dev \
libssl-dev \
libayatana-appindicator3-dev \
librsvg2-devStart the desktop app in dev mode:
npm run tauri:devBuild the desktop app:
npm run tauri:buildIf you want to build without running the dev server, use npm run tauri:build.