TeXRA

Appearance

Lean 4 Proofs ​

You're formalizing a theorem and Lean is fighting you: the proof state isn't what you expected, you can't remember the name of the Mathlib lemma you need, and the build cache is stale. TeXRA drives a real Lean 4 language server so its agents can read compiler diagnostics, inspect the proof state at any point, search Mathlib, and manage your build — all without leaving your editor.

Prerequisites ​

TeXRA doesn't ship a Lean toolchain — you bring your own. It then drives Lean in one of two ways, depending on how you run TeXRA.

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 auto-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 exact same language server, diagnostics, and proof state you see in the editor.

Install the Lean 4 extension

In the CLI ​

There's no Lean 4 extension to lean on, so TeXRA spawns its own server (lake env lean --server, one process per project). You need lake on your PATH:

  1. Install elan (the Lean version manager):
    bash
    curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
  2. Confirm it works in a fresh shell:
    bash
    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, see the Lean community install guide.

Activating Lean ​

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

Check that it's working

Open Dashboard → Tools () → 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 — one per Lake project root.

Choosing an Agent ​

The built-in lean agent is always available. The Lean Project team adds a leanOrchestrator plus the Lean specialists it delegates to (leanSearch, leanSimplifier, leanBlueprint) — all remote agents, so sign in to sync them. The team also bundles the latexFixer and progressCheck helpers.

AgentAvailabilityBest for
leanBuilt-inWriting and debugging proofs; iterating until a file compiles
leanSearchRemote / Lean teamFinding the right Mathlib lemma, exploring APIs, formalization questions
leanSimplifierRemote / Lean teamCleaning up proofs to Mathlib-quality, upstream-ready standards
leanBlueprintRemote / Lean teamBuilding dependency-tracked LeanBlueprint LaTeX that bridges math ↔ Lean
leanOrchestratorRemote / Lean teamCoordinating a whole formalization project across the agents above

To load the full set, open the Multi-Agent tab and select the Lean Project team. Formalizing a paper that's 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 Dashboard → Agents () to see exactly which tools each one has enabled.

What You Can Do ​

Just describe the task in plain language — the agent decides which tools to call. Here's what's happening under the hood: 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). Reach for 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 just the current file's imports — 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). See 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 — try fetch_cache.

The Lean Project agents aren't in my list — leanSearch, leanSimplifier, leanBlueprint, and leanOrchestrator are remote agents. Sign in and select the Lean Project team to sync them. The built-in lean agent works without signing in.

Next Steps ​