Tex2Lean

From a theorem in your paper to a working Lean 4 project.

The primary usecase (for now): you have an algorithm and a theorem about it.

That said, it should be able to handle other kind of situations as well.

Tex2Lean will formalize both, the pseudocode transcribed line by line from the paper and the theorem stated over what that pseudocode returns. And then it will prove the theorem. It should be able to identify and fix minor bugs as well in your theorems.

Download

1. (Recommended) Search for "Tex2Lean" on extensions tab and click "install".

2. Alternatively, get the latest .vsix from meelgroup/tex2lean-releases, then Extensions → the ··· menu → Install from VSIX…. Or:

code --install-extension tex2lean4.vsix

3. There is also a command line version [still in early development phase] that you can install with

curl -fsSL https://raw.githubusercontent.com/meelgroup/tex2lean-releases/main/install.sh | sh
tex2lean scan

On Windows, irm https://raw.githubusercontent.com/meelgroup/tex2lean-releases/main/install.ps1 | iex.

Quick start

First open the folder that contains the paper's Tex source files.

Tex2Lean: Open in Side bar, which will open Tex2Lean in the sidebar view. [This is similar to how you would open Codex/Claude in Sidebar].

1. You will see a button to Set Up (this needs to be done only once).

2. Click Scan LaTeX sources — the paper's main results appear in the sidebar, with everything else the scan found one click behind them.

3. Click Formalize on the result you want — or Formalize several… to tick off a batch and let it work through them one at a time. Sit back and enjoy!

Requirements

VS Code 1.90+, git (Tex2Lean installs Lean itself, but not git — that needs your system's package manager), and one of:

• a Claude Pro or Max subscription with Claude Code signed in;
• a ChatGPT Plus or Pro subscription with Codex signed in;
• an Anthropic or OpenAI API key.

PDF import works too, with pdftotext or mutool, though .tex gives a materially better blueprint.

Found a bug?

Please open an issue.

Two things make a report usable. The version, from the Extensions pane. And the log — click Log at the bottom of the side bar, and paste the part around the problem.

You can reach me at meel@gatech.edu.

=