LeanExplain — Lean 4 Natural Language Explainer

LeanExplain is a Lean 4 Infoview plugin that turns Lean declarations and proofs into natural language explanations (Chinese or English), helping users understand formal code more quickly.

LeanExplain v0.2.0

This release extends specialized explanations beyond theorems and definitions to inductive, structure, class, named instance, axiom, and opaque declarations. LeanExplain now extracts constructors, fields, inheritance, and type-class metadata from the elaborated Lean environment and routes each declaration through a dedicated Chinese or English prompt. See examples/Declarations.lean for a complete example.

LeanExplain explains formal Lean statements and proofs directly inside VS Code Infoview.

Overview

LeanExplain is an open-source tool developed by the SJTU-AI4Math team to lower the barrier to entry for formal verification. It runs as a Lean 4 Infoview plugin and leverages large language models to translate Lean declarations and proofs into readable natural language, helping researchers and students quickly grasp the content and structure of formal code.

Current environment:

Component	Version
Lean	`v4.30.0`
Python	`3.11`
mathlib4	`v4.30.0`
ProofWidgets4	`v0.0.99`

Core Features

Feature	Description
`#leanexplain` command	Explain theorems, definitions, inductive types, structures, classes, instances, axioms, and opaque definitions
Cursor-driven cache display	Display a matching cached result for the declaration under the cursor
Multi-model support	Select an OpenAI-compatible provider/model configuration with `default_provider`
Bilingual output	Set `language = "zh"` or `"en"` in `config.toml`
Brief / Detailed style	Set `style = "brief"` or `"detailed"` in `config.toml`
Local caching	Results cached under `cache/`; identical requests hit cache in seconds
Central installation	Reuse one configuration while isolating cache by project and Lean version
Management CLI	Diagnose installations and preview, list, or clean central caches

Quick Start

1. Install dependencies

# Install elan (if not already installed)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# Create Conda environment
conda create -n leanexplain python=3.11
conda activate leanexplain

2. Configure API key

cp config.example.toml config.toml
chmod 600 config.toml

Edit config.toml with your API key and model settings:

default_provider = "deepseek"
language = "zh"
style = "brief"

[providers.deepseek]
provider_type = "openai_compatible"
api_key = "your_deepseek_api_key"
base_url = "https://api.deepseek.com"
model = "deepseek-v4-pro"

[python]
executable = ""

Leave python.executable empty when python or leanexplain is available on PATH. Otherwise set the interpreter explicitly; on Windows, use forward slashes such as "C:/Users/your-name/anaconda3/envs/leanexplain/python.exe".

3. Build the project

lake update
lake build

4. Install Python package

python -m pip install -e "./python[dev]"
leanexplain doctor --home . --project-root .

5. Try the example

Open examples/example.lean in VS Code with the Lean extension enabled.

The example already imports LeanExplain, registers the Infoview panel, and contains several #leanexplain commands:

import LeanExplain
open LeanExplain

show_panel_widgets [LeanExplainPanel]

#leanexplain fermat_little_theorem_1

After the Lean server finishes loading, place the cursor inside a theorem to view any cached explanation in Infoview, or run a #leanexplain command to generate a fresh explanation.

You can also check the file from the terminal:

lake env lean examples/example.lean

Use from Another Project

LeanExplain uses a central installation mode: maintain one installation, one central config.toml, one Python environment, and one central cache directory. Other Lean projects use it through a Lake dependency. Consumer projects do not need to copy config.toml or store API keys again.

Consumer projects must currently use leanprover/lean4:v4.30.0. Before starting, make sure:

You have completed the Quick Start steps in the LeanExplain installation directory.
The LeanExplain installation directory contains a working config.toml.
The consumer project is a Lean 4.30.0 Lake project.
VS Code has the Lean 4 extension installed and enabled.

1. Make VS Code find the central installation

LEANEXPLAIN_HOME must point to the absolute path of the LeanExplain installation. Infoview is provided by the Lean server launched by VS Code, so setting export temporarily in one terminal is usually not enough for Infoview. After setting the variable, restart VS Code and the Lean server so they inherit it.

Linux

If you use Bash, edit ~/.profile:

nano ~/.profile

Add this line at the end:

export LEANEXPLAIN_HOME="$HOME/LeanExplain"

If LeanExplain is installed elsewhere, replace it with the real absolute path. Then fully quit VS Code, log out and back in to your desktop session, and reopen the consumer project.

You can also confirm the variable from a new login terminal and start VS Code there:

echo "$LEANEXPLAIN_HOME"
cd /path/to/your-lean-project
code .

Windows (native)

Create a persistent user-level environment variable in PowerShell:

[Environment]::SetEnvironmentVariable(
  "LEANEXPLAIN_HOME",
  "C:\Users\your-name\LeanExplain",
  "User"
)

Replace the path with the actual installation directory. After running this command, fully close all VS Code windows and reopen VS Code. Reloading only the Lean file is not enough to refresh the environment already inherited by the VS Code process.

Check the user-level value from a new PowerShell window:

[Environment]::GetEnvironmentVariable("LEANEXPLAIN_HOME", "User")

For Lake paths in native Windows projects, prefer forward slashes, for example C:/Users/your-name/LeanExplain.

Windows + WSL

If Lean, LeanExplain, and the consumer project all run inside WSL, set a Linux path inside WSL. Do not put a Windows path in LEANEXPLAIN_HOME.

VS Code WSL does not read ordinary shell startup files when it starts the remote server, so use the VS Code WSL environment setup script. In a WSL terminal, run:

mkdir -p ~/.vscode-server
nano ~/.vscode-server/server-env-setup

Add:

#!/bin/sh
export LEANEXPLAIN_HOME="$HOME/LeanExplain"

If the file already exists, keep its existing content and append the export line. Then run:

chmod +x ~/.vscode-server/server-env-setup

Fully close all VS Code WSL windows, then run this in Windows PowerShell:

wsl --shutdown

Finally reopen the consumer Lean project in VS Code WSL mode. This only needs to be configured once; multiple WSL projects can reuse the same LeanExplain installation.

macOS

The default macOS shell is usually Zsh. Edit ~/.zprofile:

nano ~/.zprofile

Add this line at the end:

export LEANEXPLAIN_HOME="$HOME/LeanExplain"

Fully quit VS Code with Cmd+Q, log in again, and reopen the project. To make sure VS Code inherits the Zsh environment, run Shell Command: Install 'code' command in PATH from the VS Code command palette, then start VS Code from a new terminal:

echo "$LEANEXPLAIN_HOME"
cd /path/to/your-lean-project
code .

If you use Bash, put the same export line in ~/.bash_profile.

2. Make the Lean server find the Python environment

When VS Code launches the Lean server, it usually does not activate your Conda environment automatically. To make #leanexplain work reliably inside Infoview, explicitly set the Python interpreter in the central LeanExplain config.toml.

First activate the environment where LeanExplain is installed and print the interpreter path:

conda activate leanexplain
python -c "import sys; print(sys.executable)"

Write that result into the central config.toml:

[python]
executable = "/absolute/path/to/leanexplain/python"

In TOML on Windows, prefer forward slashes:

[python]
executable = "C:/Users/your-name/anaconda3/envs/leanexplain/python.exe"

If VS Code / the Lean server already has the correct python or leanexplain on PATH, executable may stay empty. For Conda, multiple Python environments, Windows, and WSL, an absolute interpreter path is recommended.

3. Add LeanExplain to the external Lake project

Confirm that the consumer project's lean-toolchain is:

leanprover/lean4:v4.30.0

If the project uses lakefile.toml, add:

[[require]]
name = "LeanExplain"
path = "/absolute/path/to/LeanExplain"

Path examples by system:

System	`path` example
Linux or WSL	`path = "/home/your-name/LeanExplain"`
macOS	`path = "/Users/your-name/LeanExplain"`
Native Windows	`path = "C:/Users/your-name/LeanExplain"`

Only write the one path that matches your own system. This path should point to the same LeanExplain installation as LEANEXPLAIN_HOME. Personal absolute paths are not suitable for committing to shared projects; each user should change it to their own LeanExplain installation path.

If the project uses lakefile.lean, add:

require LeanExplain from "/absolute/path/to/LeanExplain"

Then run these commands from the consumer project root:

lake update
lake build

4. Show explanations in VS Code Infoview

In a Lean file where you want to use LeanExplain, import the library and register the Infoview panel:

import LeanExplain

open LeanExplain

show_panel_widgets [LeanExplainPanel]

theorem my_theorem (n : Nat) : n = n := by
  rfl

#leanexplain my_theorem

The VS Code workflow is:

Wait for the Lean server to finish loading the file.
The first run of #leanexplain my_theorem calls the model and writes to the central cache; if a matching cache already exists, it reads directly from cache.
Open Lean Infoview with Ctrl+Shift+Enter (Cmd+Shift+Enter on macOS).
Move the cursor inside the my_theorem declaration. LeanExplainPanel displays the cached explanation matching the current provider, model, language, and style.
If the current declaration has no matching cache, the panel asks you to add and run #leanexplain <declaration> first. Moving the cursor does not call the model automatically.

show_panel_widgets [LeanExplainPanel] currently needs to appear once in each Lean file where you want to use the cursor panel. Put #leanexplain only after declarations for which you want to generate explanations.

5. Verify the VS Code environment

If Infoview shows LeanExplain home was not found, temporarily add this line to a Lean file:

#eval IO.getEnv "LEANEXPLAIN_HOME"

The normal output should look like:

some "/absolute/path/to/LeanExplain"

If it prints none, the variable exists only in your terminal and was not inherited by the current VS Code / Lean server process. Recheck the setup for your operating system and fully restart VS Code; WSL users should also restart WSL. Remove the #eval line after verification.

You can also run this in the VS Code integrated terminal of the consumer project:

leanexplain doctor --project-root .

The report shows the resolved mode, installation directory, config/cache paths, Python and Lean versions, consumer toolchain, provider names, and whether the default API key is configured. It never prints the API key itself.

API and Widget caches are stored centrally under:

LeanExplain/cache/projects/<project-id>/lean-v4.30.0/

The project ID includes a hash of the normalized consumer project path, so projects containing declarations with the same name remain isolated.

Configuration

config.example.toml is the tracked template included in the repository. It documents the available options but should not contain real API keys.

From the LeanExplain installation root, create your private configuration from the template:

cp config.example.toml config.toml
chmod 600 config.toml

config.toml lives at the LeanExplain installation root and is ignored by .gitignore, so each user can keep their own API keys and local paths without committing them. External consumer projects reuse this central file.

The default template looks like this:

default_provider = "deepseek"
language = "zh"
style = "brief"
timeout_seconds = 300.0
max_completion_tokens = 4096
call_attempts = 3
cache_enabled = true

[providers.deepseek]
provider_type = "openai_compatible"
api_key = "your_deepseek_api_key"
base_url = "https://api.deepseek.com"
model = "deepseek-v4-pro"

[python]
executable = ""

Main options

Option	Meaning
`default_provider`	The provider entry used by default. With the template above, LeanExplain uses `[providers.deepseek]`.
`language`	Output language for `#leanexplain`: `"zh"` or `"en"`.
`style`	Explanation style: `"brief"` for concise output or `"detailed"` for more expanded output.
`timeout_seconds`	Timeout for each model request. Increase this if your model endpoint is slow.
`max_completion_tokens`	Maximum response length requested from the model. LeanExplain sends this field by default and maps it to `max_tokens` only for endpoints that require the older name, including the official DeepSeek API.
`call_attempts`	Number of retry attempts for a model request.
`cache_enabled`	Whether the Python CLI should read/write API cache files under the central project/version cache directory.

Provider options

Option	Meaning
`provider_type`	API format. LeanExplain currently supports only `"openai_compatible"`; this field may be omitted because that is the default.
`api_key`	Your API key. You may also leave it empty and set `LEANEXPLAIN_DEEPSEEK_API_KEY` in the environment.
`base_url`	Model service base URL. DeepSeek official API uses `https://api.deepseek.com`.
`model`	Model name sent to the provider. Change this when your provider uses a different model ID.

All provider entries use the OpenAI Python SDK and the Chat Completions API shape. To switch vendors, keep provider_type = "openai_compatible" and change api_key, base_url, and model. default_provider selects the named entry; it does not select an API implementation.

To add another provider, create a new section and point default_provider to it:

default_provider = "my_provider"

[providers.my_provider]
provider_type = "openai_compatible"
api_key = "your_api_key"
base_url = "https://example.com/v1"
model = "your-model-name"

For this provider, the matching environment variable would be LEANEXPLAIN_MY_PROVIDER_API_KEY.

Python option

[python].executable controls which Python interpreter Lean uses when it launches the CLI. Leave it empty when python or leanexplain is available on PATH.

On Windows or multi-environment machines, set it explicitly:

[python]
executable = "C:/Users/your-name/anaconda3/envs/leanexplain/python.exe"

You can also override it with the environment variable LEANEXPLAIN_PYTHON.

Widget caches are isolated by provider, model, language, style, and task. Changing any of these settings makes the cursor panel look up the matching cache; switching back reuses the earlier result. Legacy <declaration>.json files remain for compatibility but are not treated as configuration-specific cursor cache hits.

Diagnostics and Cache Management

doctor returns a nonzero exit code when the installation, configuration, API key, active Lean executable, or consumer Lean version is unusable:

leanexplain doctor --home "/absolute/path/to/LeanExplain" --project-root .

List central project caches and their complete project IDs:

leanexplain cache list
leanexplain cache list --json

Cache cleanup is preview-only unless --yes is supplied:

# Preview one project
leanexplain cache clean --project <project-id>

# Delete it after reviewing the preview
leanexplain cache clean --project <project-id> --yes

# Preview only the Lean 4.30.0 cache for every project
leanexplain cache clean --all --lean-version 4.30.0

Pass --home "/absolute/path/to/LeanExplain" to any cache command when LEANEXPLAIN_HOME is not set. Deleting cache never removes config.toml, but currently open VS Code windows may need to refresh before showing the new cache state.

Upgrading

After pulling a new LeanExplain version, refresh both the Python package and Lean build products:

cd /path/to/LeanExplain
conda activate leanexplain
git pull
python -m pip install -e "./python[dev]"
lake update
lake build
leanexplain doctor --home . --project-root .

Consumer projects should then run lake update and lake build once. They continue to use the same central config.toml.

When a request misses the new namespaced cache, LeanExplain checks the old cache/api/ and cache/widget/ locations in read-only mode. A matching entry is copied into cache/projects/<project-id>/lean-v4.30.0/; the old file is not moved or deleted. Keep old caches until the upgraded installation has successfully displayed the expected results.

For release validation from a clean source snapshot, maintainers can run:

python scripts/verify_release.py

The script builds LeanExplain, runs Python and Lean regression tests, checks doctor, and creates a temporary external Lean 4.30.0 project. It does not call a model.

Usage Examples

Command mode

Import LeanExplain in a Lean file and run the #leanexplain command:

import LeanExplain

theorem add_comm (a b : ℕ) : a + b = b + a := by
  induction a with
  | zero => simp
  | succ a ih => simp [add_succ, ih]

#leanexplain add_comm

The first run calls the model to generate an explanation, displayed in Infoview. Running the same command again reads directly from cache.

See examples/Declarations.lean for complete inductive, structure, class, named instance, axiom, and opaque examples.

Cursor-driven mode

Register the panel once near the top of the Lean file:

import LeanExplain
open LeanExplain

show_panel_widgets [LeanExplainPanel]

Move your cursor inside any supported named declaration. Specialized explanations are currently available for:

theorem / lemma
def / abbrev
inductive
structure
class
named instance
axiom
opaque

The Infoview panel will automatically:

Check the cache for an existing explanation.
Cache hit → display immediately.
Cache miss → show the matching #leanexplain command; run it manually to generate the explanation.

Use show_panel_widgets [LeanExplainPanel] as the single panel entry; an additional #widget LeanExplainPanel is unnecessary. Moving the cursor never calls a model automatically.

Project Structure

LeanExplain/
├── LeanExplain/
│   ├── Command/Explain.lean      # #leanexplain command entry
│   ├── Extract/                  # Context extraction (declaration, proof, cursor)
│   ├── Config/                   # Configuration loading (TOML parsing, defaults)
│   ├── Cache/                    # Caching (key generation, path, JSON read/write)
│   ├── Runtime/                  # Central home, consumer project, paths, Lean version
│   └── Widget/                   # Infoview panel (cursor lookup and cache rendering)
├── python/lean_explain/
│   ├── runtime.py                # Python-side home and Lean version diagnostics
│   ├── cache_admin.py            # Cache listing and guarded cleanup
│   ├── providers/                # OpenAI-compatible model integration
│   ├── templates/                # Prompt templates (Chinese / English)
│   ├── eval/                     # Evaluation dataset and runner
│   └── cli.py                    # CLI entry point
├── cache/projects/               # Project- and Lean-version-isolated caches
├── scripts/verify_release.py     # Clean deployment/release verification
├── config.toml                   # Local config (not committed)
├── config.example.toml           # Config template
└── examples/                     # Example files

License

LeanExplain is released under the Apache License 2.0.

Navigation Menu

Uh oh!

Repository files navigation

LeanExplain — Lean 4 Natural Language Explainer

Table of Contents

Overview

Core Features

Quick Start

1. Install dependencies

2. Configure API key

3. Build the project

4. Install Python package

5. Try the example

Use from Another Project

1. Make VS Code find the central installation

Linux

Windows (native)

Windows + WSL

macOS

2. Make the Lean server find the Python environment

3. Add LeanExplain to the external Lake project

4. Show explanations in VS Code Infoview

5. Verify the VS Code environment

Configuration

Main options

Provider options

Python option

Diagnostics and Cache Management

Upgrading

Usage Examples

Command mode

Cursor-driven mode

Project Structure

License

About

Releases

Packages

Contributors

Languages

Name		Name	Last commit message	Last commit date
LeanExplain		LeanExplain
cache		cache
docs		docs
examples		examples
python		python
scripts		scripts
tests		tests
.gitignore		.gitignore
LICENSE		LICENSE
LeanExplain.lean		LeanExplain.lean
README.md		README.md
README.zh.md		README.zh.md
config.example.toml		config.example.toml
lake-manifest.json		lake-manifest.json
lakefile.lean		lakefile.lean
lean-toolchain		lean-toolchain

Uh oh!

Latest commit

History

Folders and files

Repository files navigation

LeanExplain — Lean 4 Natural Language Explainer

Table of Contents

Overview

Core Features

Quick Start

1. Install dependencies

2. Configure API key

3. Build the project

4. Install Python package

5. Try the example

Use from Another Project

1. Make VS Code find the central installation

Linux

Windows (native)

Windows + WSL

macOS

2. Make the Lean server find the Python environment

3. Add LeanExplain to the external Lake project

4. Show explanations in VS Code Infoview

5. Verify the VS Code environment

Configuration

Main options

Provider options

Python option

Diagnostics and Cache Management

Upgrading

Usage Examples

Command mode

Cursor-driven mode

Project Structure

License

About

Topics

Resources

Stars

Watchers

Forks

Releases

Packages

Contributors

Languages