Tex2Lean for VS Code
Tex2Lean is a VS Code extension for formalizing results from LaTeX papers in Lean 4. It uses AI to translate the model and algorithm and develop proofs. You review the generated statements and assumptions.
Supports papers with algorithms and claims about their output.
Theorem 1.
For every admissible input, the algorithm returns an output satisfying the stated guarantee.
-- Schematic statement
theorem output_guarantee
(x : Input) (h : Admissible x) :
Guarantee (algorithm x) :=
by …
Search for Tex2Lean in VS Code’s Extensions
view and select Install. Open the folder
containing your paper’s .tex files, including any
files it imports.
Open the command palette and run:
Tex2Lean: Open in Side bar
Prefer a manual install? Download a .vsix from
GitHub Releases, then choose
Extensions → ··· → Install from VSIX….
Choose Connect and select your intended model connection. A signed-in Claude Code or Codex CLI is the simplest route for planning and proof agents. API connections are also available for planning and review; coding agents still need a CLI.
Select Set Up. Follow the setup prompts and wait for the Lean environment to be ready. Tex2Lean fetches, indexes, and builds the libraries, reusing compatible setup where possible.
Select Scan LaTeX sources. Check that Tex2Lean is reading the intended root paper, then use a result’s source link to inspect what it found. Select Formalize beside one result.
For a specific excerpt, select the statement in a
.tex editor, right-click, and choose
Tex2Lean: Formalize the selected statement.
When Tex2Lean asks you to review the statement before proving,
inspect Model/Theorem.lean and the relevant model
files. Compare the inputs, quantifiers, hypotheses, algorithm,
and conclusion with your paper.
If it matches, choose the card’s option to start proving. If
it does not, edit the Lean file and press
Resume, or type /change in chat
and describe the correction.
Lean checks the statement you encode. Your review establishes whether that statement captures the result you intended.
Follow the Planning, Interface, and Proof milestones. Agents work on proof obligations and build their changes with Lean. Read any questions or findings that need your attention.
Ask a question in chat to understand the current development. Use Pause to stop active work and save a resumable checkpoint. Wait for cleanup to finish before editing; Resume continues from the work already saved.
Inspect the result’s current Lean check and the handoff
findings. Check that the theorem no longer depends on
sorryAx, and read any explicit prior-work
hypotheses.
A successful build is one part of the evidence. Review the complete result checklist before treating the development as finished.
The formalization connects the algorithm, its mathematical meaning, and its resource bounds through three layers.
Define the inputs, operations, algorithm, and theorem. For
time-complexity claims, write the algorithm using the
Charged interface: each computation carries its
result and a tally of the operations it performs.
Model/Definitions, program, and theorem
Prove the connection between the implemented program and the mathematical representation used in the analysis. This lets the proof reason about the algorithm at a convenient level while keeping the theorem tied to the modeled program.
Interface/Program-to-analysis connection
Prove correctness and resource bounds for the modeled program. The time theorem bounds its accumulated charges; for a randomized algorithm, expected time is stated over the distribution of charged runs.
Analysis/Proofs and resource bounds
Read the formal statement, the proof evidence, and what the development assumes.
A machine-checked proof establishes the encoded theorem under its stated hypotheses. It does not, by itself, establish that the translation says exactly what the paper says.
Inspect the model definitions and program as well as the theorem. Check every assumption and conclusion.
Lean’s standard axioms—propext,
Classical.choice, and Quot.sound—can
appear in a valid proof. Additional axioms need scrutiny. Read
Model/Prior.lean: its hypotheses remain conditions
of the result even when the proof is sorry-free.
Review the mechanical checks and the paper comparison. Treat ambiguities, changed hypotheses, and reported defects as findings to inspect.
How time is counted
Standard charged operations come from arlib. When a paper needs
operations that arlib does not support,
Model/Operations.lean defines those additional
primitives and their cost model. In
Model/Program.lean, the algorithm calls its
operations through Charged. Sequential steps add
their charges, loops accumulate the charges of their iterations,
and a branch contributes the work it executes.
Sealed data interfaces and program checks require work such as dictionary updates, size tests, and scan visits to go through charged operations. The time bound is then proved about the tally produced by this program.
Click Blueprint at the top of the sidebar to explore two maps: your paper’s statements and the Lean modules that formalize them. Follow their dependencies and connections between LaTeX source locations and Lean files. Click a node to inspect its details.
Click Settings to change your model connection, choose a model, and set Agents at once for parallel work. Agent-count changes during a run apply at the next round. Use Auto-answer routine decisions to let Tex2Lean handle routine choices automatically.
Save a theorem or lemma with a
sorry proof under your project’s Model/.
It appears in Lean statements; choose
Prove to work on the declaration directly. No
paper scan is required.
Use Formalize several… to choose a group. Tex2Lean writes the selected statements and shared vocabulary before entering the long proof phase. Each theorem keeps its own checkpoint.
Click Open Chat in the Tex2Lean sidebar to ask questions about your paper, understand the formalization, and explore the current proof state.
When ready, use Donate Lean in Settings to propose the project to arlib-community. Review the material and acknowledgement before publishing. Community contributions go through a pull request.
You can start with a paper and the guided workflow. You still need to review the generated statement and assumptions. If you cannot assess the Lean translation, work with someone who can before relying on the result.
Yes, through
Tex2Lean: Import from PDF (discouraged), when
pdftotext or mutool is installed.
LaTeX is preferred: PDF extraction can lose notation and
mathematical structure, so review the extracted statement
carefully.
Connect supports a signed-in Claude Code or Codex CLI, or API providers including Anthropic, OpenAI, and OpenRouter. Choose the provider explicitly when that is your intended route.
API providers can run planning and review passes. Agents that edit and build Lean use a configured Claude Code or Codex CLI, so keep one available for the complete workflow. A subscription connection uses the CLI’s account and allowance; API credentials use provider billing.
API keys entered in the extension are stored in VS Code SecretStorage, rather than plain-text settings. The selected model connection receives paper excerpts and relevant development context. Coding agents can inspect project files. Review your provider’s data policies and only use material you are permitted to share.
It depends on the paper, model connection, library reuse, and proof difficulty. Initial setup needs downloads and builds; formalization can run for hours. The sidebar shows usage where available.
Choose Pause in the pinned run control. Tex2Lean stops active work, keeps generated files, and records a paused checkpoint. Allow cleanup to finish. Use the result’s Resume control when you are ready to continue; reopen the same project folder if you closed VS Code.
Papers often use results from prior work. Tex2Lean can record
those as explicit hypotheses in Model/Prior.lean.
A proof can be complete relative to these hypotheses without
proving them here. Read the Prior Work entries, citations, and
theorem binders; use the assumptions command if you want to
discharge more of them.
Yes. Open its folder and use the
Lean statements list for saved theorem and
lemma declarations under Model/. Choose
Prove for a statement with
sorry. Tex2Lean checks and proves the existing
declaration without restating it from TeX.
For setup, follow the reported action and check Git, disk space, network access, and the toolchain information. For an empty scan, check the selected root paper and its included files. Try the selected-statement context menu for a specific result. Use Tex2Lean: Show extension log for details.
Yes, an experimental CLI is distributed through
the release repository, with shell instructions for macOS/Linux and PowerShell
instructions for Windows. Run tex2lean --help for
available commands. This tutorial focuses on the VS Code
extension.
Reporting issues
Report an issue with your Tex2Lean version and the relevant output from Tex2Lean: Show extension log. Remove private information before posting.