Lean 4 proofs

Formalizing mathematics requires continuous feedback: inspecting proof states, identifying Mathlib lemmas by signature, resolving compiler errors, and managing build caches. TeXRA connects directly to a running Lean 4 language server, allowing agents to read compiler diagnostics, inspect goal states at any position, search Mathlib via Loogle, and trigger project builds from within your workspace.

Prerequisites

TeXRA relies on your local Lean toolchain, interfacing with it through one of two mechanisms depending on the host environment:

You always need a Lake project

Lean tools only work on .lean files that live inside a Lake project: a folder (or ancestor folder) containing a lakefile.lean or lakefile.toml. If there's no lakefile, the language server has nothing to attach to. Create one with lake new myproject or lake init.

In VS Code

1. Install the official Lean 4 extension (leanprover.lean4) from the Marketplace.
2. Open a folder containing a lakefile.lean or lakefile.toml.
3. The Lean 4 extension installs elan and the Lean toolchain on first open.

TeXRA detects the running Lean 4 extension and routes its tools through it, so you share the same language server, diagnostics, and proof state you see in the editor.

Install the Lean 4 extension

In the CLI

Without the VS Code extension host, the CLI spawns and manages its own headless server process (lake env lean --server). Each Lake project receives a dedicated process that terminates when its calling run ends (or after an idle timeout of 30 minutes). Ensure lake is present on your PATH:

1. Install elan (the Lean version manager):

   curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

2. Confirm it works in a fresh shell:

   lake --version

3. Open a folder containing a lakefile.lean or lakefile.toml.

texra chat

$texra chat --agent lean

›Check Proofs/GroupTheory.lean for errors.

starting lake env lean --server (one per Lake project)

●lean_diagnostics(Proofs/GroupTheory.lean)

⎿1 error — line 42: unknown identifier 'mul_com'

No extension underneath: the CLI talks to Lake directly, and the same lean_* tools run against its own server process.

If you don't have elan yet, follow the Lean community install guide.

Activating Lean

There is no switch to flip. Lean support turns on the moment a Lean-capable agent runs a Lean tool on a .lean file in a Lake project. Pick a Lean-capable agent (see below) and ask it to work on your proof.

Check that it's working

Open Settings → Plugins () → Lean 4 Proof Assistant () to confirm your setup is detected. The panel shows whether the Lean 4 extension is available (VS Code) or whether lake was found (CLI), and lists any active language servers.

Choosing an agent

All the Lean agents ship with TeXRA and need no sign-in. The lean agent handles day-to-day proof work. The Lean Project team adds a leanOrchestrator plus the Lean specialists it delegates to (leanSearch, leanSimplifier, leanBlueprint), and also bundles the latexFixer and progressCheck helpers.

Agent	Availability	Best for
lean	Built-in	Writing and debugging proofs; iterating until a file compiles
leanSearch	Built-in / Lean team	Finding the right Mathlib lemma, exploring APIs, formalization questions
leanSimplifier	Built-in / Lean team	Cleaning up proofs to Mathlib-quality, upstream-ready standards
leanBlueprint	Built-in / Lean team	Building dependency-tracked LeanBlueprint LaTeX that bridges math ↔ Lean
leanOrchestrator	Built-in / Lean team	Coordinating a whole formalization project across the agents above

To load the full set, open the Teams tab and select the Lean Project team. If you're formalizing a paper that is also part LaTeX, the Mathematician team bundles the lean agent alongside the LaTeX and research agents.

TIP

Pick any agent from the Agent dropdown (). Check Settings → Agents () to see which tools each one has enabled.

What you can do

Describe the task in plain language; the agent decides which tools to call. Below are the five Lean tools the agent reaches for, as they surface in the tool-call log.

leantool calls · this run

Read diagnostics · lean_diagnostics✓ 0 errors

Inspect the proof state · lean_inspect⊢ goal

fileAnalysis/Limits.lean

positionline 42

kindgoal

result⊢ Continuous (f + g)

Search Mathlib · lean_loogle0:02

Refresh a stuck file · lean_file0:05

Manage the project · lean_project1:48

The agent picks the tool (read diagnostics, inspect the proof state, search Mathlib, refresh a file, or manage the build) and you watch each call land in the run log.

Read diagnostics

Check Proofs/GroupTheory.lean for errors and fix the first one.

The lean_diagnostics tool reports compilation errors, type mismatches, unsolved goals, warnings, and hints with their locations. Use it to check whether a file compiles after each change.

Inspect the proof state

What's the goal state at line 42 of Analysis/Limits.lean?

The lean_inspect tool reads the tactic proof state (goal), the expected type in term mode (term_goal), or the type signature and docs of an identifier (hover) at a given position: the same information Lean shows in its infoview.

SpectralGap.leanlean_diagnostics

theorem spectral_gap_pos (hd : 2 ≤ d) :

d - mu2 G > 0 := by

sorry

error: line 3 — unsolved goals

⊢ d - mu2 G > 0

agent inspects the goal, finds the lemma, iterates

λSpectralGap.leancompiles

theorem spectral_gap_pos (hd : 2 ≤ d) :

d - mu2 G > 0 := by

have hμ : mu2 G < d := alon_boppana hd

linarith

✓ proof compiles · 0 errors · 0 sorry

The agent reads the unsolved-goals diagnostic, inspects the goal state, finds the right lemma, and iterates the proof until it compiles with 0 errors and 0 sorry.

Search Mathlib

Find a Mathlib lemma that says the sum of two continuous functions is continuous.

The lean_loogle tool queries Loogle to find lemmas by name, type signature, or the constants they mention, so the agent cites real Mathlib lemmas instead of inventing them.

Refresh a stuck file

The diagnostics for this file look stale. Restart the Lean server for it.

The lean_file tool runs file-scoped commands: restart (reload the language server for one file) and refresh_dependencies (a lighter refresh). Use these when results look out of date.

Manage the project

Download the Mathlib build cache, then build the project.

The lean_project tool runs project-wide commands without a target file, grouped into server control, build operations, and toolchain setup:

lean_projectproject-wide commands · no target file

Server

restart_serverstop_server

Build

buildcleanfetch_cachefetch_file_cache

Setup VS Code only

install_elanupdate_elaninstall_depsselect_toolchain

Server and build commands run everywhere; the Setup group drives the Lean 4 extension's installers, so it's gated to VS Code. fetch_cache pulls the whole project; fetch_file_cache covers only the current file's imports, which is faster.

Setup commands are VS Code-only

The setup commands drive the Lean 4 extension's installers, so they only work in the VS Code build. In the CLI they fail with a "run the shell command directly" message. Manage your toolchain with elan and lake directly instead (for example elan self update, elan toolchain install, or lake update). Follow the Lean install guide.

Build output

lean_project's build command starts a build but doesn't capture its output. To see errors afterward, the agent runs lean_diagnostics on the relevant files (or lake build directly via the bash tool when it needs the raw log).

Troubleshooting

"No Lean project found": the file isn't inside a Lake project. Make sure a lakefile.lean or lakefile.toml exists in the file's folder or an ancestor. Create one with lake new / lake init.

"Failed to spawn lake env lean --server" (CLI): lake isn't on your PATH. Install elan and confirm lake --version works in a fresh shell.

Tools fail in VS Code: install the Lean 4 extension (leanprover.lean4) and open the project so its language server starts.

Diagnostics look stale: ask the agent to run lean_file with restart, or lean_project with restart_server. A missing Mathlib cache can also cause long stalls; run fetch_cache.

The Lean Project agents aren't in my list: leanSearch, leanSimplifier, leanBlueprint, and leanOrchestrator are built in, but your current team may hide them. Select the Lean Project team, or show them one by one from the Agents tab.

Next steps

• Built-in agents: full reference for the lean agent and others
• Research tools: literature search, citations, and Wolfram verification
• Agent architecture: how the orchestrator coordinates multi-agent runs