Tex2Lean
Tex2Lean turns mathematical results from a paper into a Lean 4 project. It is
designed primarily for papers that state an algorithm and prove a theorem about
its output.
For each selected result, Tex2Lean:
- reads the paper's LaTeX source;
- translates the relevant pseudocode and mathematical model into Lean;
- states the result against the translated program;
- builds and checks the proof with Lean; and
- reports ambiguities or defects that require the author's input.
Install
Search for Tex2Lean in the VS Code Extensions view and select Install.
You can also download the latest .vsix from
meelgroup/tex2lean-releases
and choose Extensions → ··· → Install from VSIX….
From a terminal:
code --install-extension tex2lean4.vsix
Get started
Open the folder containing your paper's .tex files, then run
Tex2Lean: Open in Side bar from the command palette.
- Select Set Up. This installs and builds the Lean environment and is
normally required only once per machine.
- Select Scan LaTeX sources. Tex2Lean lists the main results it found in
the paper.
- Select Formalize next to a result. To process multiple results in
sequence, select Formalize several….
LaTeX source produces the best results. PDF import is also available when
pdftotext or mutool is installed.
Saved theorem and lemma declarations under the Lean project's Model/
directories also appear in Lean statements. Declarations already linked to
paper statements keep their existing paper rows. For a new theorem, write its
statement with a sorry proof, save the file, and select Prove. Tex2Lean
checks the declaration with Lean and proves it directly, without restating it
from TeX. The row supports Resume, Recheck Lean, and navigation to its
declaration. This also works without a paper scan. Use Refresh Lean statements
if you need to refresh the list manually.
The Lean project directory is recorded in formalize.json in the paper folder,
shared by the extension and CLI. A new project uses lean/ if that name is free,
otherwise lean-2/, lean-3/, and so on. Later runs reuse the recorded choice.
Saved runs retain their checkpoint's directory. To choose an existing project
explicitly, set "lean.projectPath": "your-directory" in formalize.json or
use the CLI's --lean your-directory option. If VS Code discovers more than one
possible project, it asks which directory to use, records that choice in
formalize.json, and continues activating. VS Code workspace and global settings
no longer select the Lean project directory. Reload the editor after manually
changing the project settings file.
The same file records the Lean, Mathlib, and arlib pins for that paper under
lean.toolchain, lean.mathlibRev, lean.arlibUrl, and lean.arlibRev. Both
the extension and CLI read those project pins before user/profile defaults. On
the first run after upgrading an older paper, Tex2Lean adopts the declarations
already in lean-toolchain and the Lakefile; it does not run Lake or rewrite
either file. An existing recorded pin that disagrees with an authored Lean file
is refused until both are updated explicitly as one migration. Extension and
profile defaults therefore choose versions for new papers only.
OpenRouter is available under Connect → OpenRouter key. Save your key there
and set formalize.openrouter.model to a model slug from the
OpenRouter catalog, or leave it as openrouter/auto.
For the CLI, set OPENROUTER_API_KEY and use
--provider openrouter --model <model-slug>. Selecting OpenRouter uses @openrouter/agent for proof workers and project chat,
with local file and Lean tools; no Claude or Codex CLI is required. Selecting
Claude CLI or Codex CLI uses that CLI. OpenRouter also handles planning and review
passes. Choose a model that supports tool calling.
Requirements
- VS Code 1.90 or newer
- Git
- One supported model connection:
Tex2Lean installs Lean, but it does not install Git. The initial Mathlib build
can take some time and requires several gigabytes of disk space.
Project-aware chat
When Codex or Claude Code is available, questions in the run chat go directly
to that coding agent. It can inspect the current paper, Lean sources, proof
state, and run evidence before answering, but question turns are read-only.
Explicit change requests—and follow-ups such as do it after a proposed next
step—first ask you to pause any active Tex2Lean run. No editing agent starts
until the run is paused; you can then retry the preserved request with
Change this. The write turn runs inside Tex2Lean's checked change workflow.
The agent treats each library's Model/ directory as the user-facing audited
contract: definitions, assumptions, program semantics, and theorem statements.
Interface/ bridges that contract to proof representations, while Analysis/
contains proof implementation. Changes are rebuilt and checked for scope before
they are kept.
Command-line version
An experimental command-line version is available for macOS and Linux:
curl -fsSL https://raw.githubusercontent.com/meelgroup/tex2lean-releases/main/install.sh | sh
tex2lean scan
On Windows, run the following in PowerShell:
irm https://raw.githubusercontent.com/meelgroup/tex2lean-releases/main/install.ps1 | iex
Run tex2lean --help to see the available commands.
Tex2Lean prepares formalization.yaml inside the configured Lean project folder
(default: lean/formalization.yaml) using the
formalization.yaml standard
(v0.4). New formalizations record the source location, headline declaration,
and model used. Existing projects can run Tex2Lean: Prepare formalization.yaml
or tex2lean metadata --project /path/to/paper. This does not compile or edit proofs.
To supply project authors, license, and bibliographic details before generation,
add project-specific metadata to formalize.json:
{
"formalization.metadata": {
"project": {
"authors": ["Your name"],
"license": "MIT"
},
"sources": [{
"title": "Paper title",
"authors": ["Paper author"],
"id": "https://example.org/paper",
"relationship": "formalizes"
}]
}
}
Choose the license that actually applies to your development. Tex2Lean validates
new metadata against the upstream schema; missing required information produces
a marked draft and a list of fields to complete. It never infers authorship,
endorsement, proof counts, costs, or successful independent verification.
The initial review status is unchecked; assess it before publication.
Paths in the metadata are relative to that Lean project folder; paper sources may
therefore use ../. The workspace-root formalize.json still supplies settings.
An existing metadata file in the Lean folder is preserved byte for byte, including on Resume;
edit it directly to add later results or update its reporting. The schema comment
supports editor validation, and the upstream README provides a validation command.
Independent proof verification
Tex2Lean generates a Comparator
bundle during final handoff, after Lean's axiom query confirms that the exported
theorems use only standard Lean axioms (propext, Quot.sound, and
Classical.choice, or a subset). Unfinished proofs, custom axioms, and unanswered
queries do not qualify. It lives under <Lean project>/comparator/<fully-qualified-declaration>/, outside the development's
ordinary source modules. Its challenge preserves the theorem statements and
replaces proofs using Lean-certified syntax ranges. Proof-side imports are
removed; the generated challenge must retain the same kernel types.
For an existing project, run Tex2Lean: Prepare Comparator verification, or:
tex2lean comparator Esa22Copy.esa22copy_main
With no declaration argument, the CLI uses the first recorded headline. The
fully qualified name (for example, CountingMatroid.countingmatroid_main) keeps
the same baseline across subsequent handoffs. Valid
older hashed bundles and bundles under <output>/comparator/ are copied to this location without
regenerating their challenge; the originals remain preserved.
The bundle includes a frozen baseline/, contract.json, and prepare.py. Review
the challenge, its trusted imports, and the Lake configuration independently.
To snapshot the current solution without compiling it:
python3 /path/to/bundle/prepare.py --source /path/to/lean/project
New preparation scripts place temporary solution captures in the Lean project's
.blueprint/comparator-exports/; use --exports /path/to/captures to choose
another directory. Migrated scripts remain unchanged. The comparator/ tree
is excluded from proof inventories and solution captures, so challenge placeholders
do not count as unfinished development proofs.
The script prints a fresh export directory. On an unprivileged Linux account,
resolve its dependencies from the copied lake-manifest.json without running
lake update, use a trusted Mathlib cache if needed, then run:
sh verify.sh /absolute/path/to/comparator
Comparator requires real Landrun and a lean4export compatible with the project's
Lean version; COMPARATOR_LANDRUN and COMPARATOR_LEAN4EXPORT can specify their
paths. The runner uses upstream's systemd-run restriction. Do not compile the
solution in that checking environment before Comparator. Generating a bundle
does not mean verification passed.
Resume preserves the challenge. Changed trusted definitions or configuration
stop preparation, and changed statements are checked against the old challenge.
After explicitly reviewing a replacement contract, archive the entire old
bundle under another directory name before preparing a new one; preserve its
previous captures. Definition holes are not generated. Local path dependencies
must be replaced with pinned, portable dependencies before exporting.
Report a problem
Open an issue
and include:
- the Tex2Lean version shown in the Extensions view; and
- the relevant portion of the extension log, available through
Tex2Lean: Show extension log or the Log button in the side bar.
Please review the log before posting it and remove any information you do not
want to share publicly.
Questions can also be sent to meel@gatech.edu.
