Tex2Lean

A guide for paper authors

From a paper
to a Lean proof.

Bring your mathematical results into Lean 4. Tex2Lean uses AI to read your LaTeX, translate the model and algorithm, and work toward a machine-checked proof—with you reviewing what is claimed.

Install for VS Code Follow the tutorial

Built for papers that state an algorithm and prove a result about its output.

PAPER → FORMALIZATION
paper.tex LaTeX

Theorem 1.

For every admissible input, the algorithm returns an output satisfying the stated guarantee.

Read · translate · review
Model/Theorem.lean Lean 4 
-- Schematic statement
theorem output_guarantee
    (x : Input) (h : Admissible x) :
    Guarantee (algorithm x) :=
  by …
Next: prove the reviewed statement
Illustrative workflow. The code above is schematic, not a complete proof.
One development, from source to evidence.
LaTeXLean 4Mathlib+ arlib

01 / Getting started

Your first formalization.

Start with one result. Review its Lean statement before moving on to the proof.

  1. Install the extension & open your paper

    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….

  2. Connect your model & set up Lean

    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.

    Check the selected connection before starting. API billing and subscription allowances come from your provider.

  3. Scan your sources & choose a result

    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.

  4. Review what the Lean theorem says

    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.

    The important checkpoint

    Lean checks the statement you encode. Your review establishes whether that statement captures the result you intended.

  5. Let the proof run—and stay in the loop

    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.

    Proof work may take hours. Watch the usage display and your provider’s allowance; a successful proof is not guaranteed.

  6. Check the proof & read the assumptions

    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.

02 / How it works

A readable claim.
A checkable argument.

Tex2Lean separates what the paper claims from the machinery used to prove it.

Stage 01

Planning

Read the paper, identify assumptions, and write the definitions, algorithm, and selected theorem into Lean.

Model/The contract you review
Stage 02

Interface

Where needed, connect the implemented program to the mathematical representation used in the proof.

Interface/The connection that must be proved
Stage 03

Proof

Break down the argument, reuse library results, and work through the remaining obligations with Lean.

Analysis/The proof implementation
Meta/

Mechanical checks run across the development: the model boundary, program constraints, and audit evidence.

03 / Reviewing results

What does “proved” mean?

Read the formal statement, the proof evidence, and what the development assumes.

Lean checks the proof.
You check the meaning.

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.

For randomized algorithms, review the distribution and probability guarantee. For resource bounds, review which operations and costs the theorem actually counts.

  1. The statement matches your paper

    Inspect the model definitions and program as well as the theorem. Check every assumption and conclusion.

  2. The current Lean evidence is complete

    Build the project and recheck the theorem. A theorem that reaches sorryAx still depends on an unfinished proof. An unanswered check is unverified.

  3. The dependencies are explicit

    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.

  4. The handoff findings are resolved

    Review the mechanical checks and the paper comparison. Treat ambiguities, changed hypotheses, and reported defects as findings to inspect.

04 / Go further

Keep building on your work.

Prove a Lean statement

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.

Select several results

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.

Explore & ask questions

Click Open Chat in the Tex2Lean sidebar to ask questions about your paper, understand the formalization, and explore the current proof state.

Share a Lean development

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.

05 / FAQ

A few good
questions.

Practical answers before your first run—and after it.

Browse reported issues
Do I need to know Lean to get started?

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.

Can I use a PDF instead of LaTeX?

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.

Which model connections can I use?

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.

Where are my API keys and paper sent?

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.

How long does a run take, and what does it cost?

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.

How do I pause and come back later?

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.

Where cancellation is offered, it also stops active work and preserves generated files. Use Resume for an available checkpoint. Reset project state is a separate destructive action and is not needed to pause.

Why does a proved theorem still have assumptions?

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.

Can I use an existing Lean project?

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.

What if setup fails or the scan finds nothing?

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.

Is there a command-line version?

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.

Need a hand?

Report an issue with your Tex2Lean version and the relevant output from Tex2Lean: Show extension log. Remove private information before posting.

Report an issue meel@gatech.edu