Tex2Lean

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

Point this at your .tex sources, pick a result, and get a complete blueprint — the statement restated in Lean, a reuse map onto Mathlib and arlib, a layered architecture.

What you get


Reads your real sources	Follows `\input`/`\include`/`\subfile`, picks up your own `\newtheorem` names, pulls in the proof, setup, and everything the statement `\ref`s
Five focused passes	Restate → reuse → architect → lay out → brief
Plain Markdown output	`BLUEPRINT.md`, `blueprint.json`, `tasks/NN-*.md` — diffable, reviewable, yours
One-click scaffold	A lake project pinned to your Mathlib and arlib revisions, skeleton and audit checks in place

Quick start

Formalize: Connect Claude or ChatGPT — your key goes into the OS keychain, never into settings or your workspace.
Formalize: Scan LaTeX sources — your theorems appear in the sidebar.
Pick one, hit the rocket, review, scaffold.

Bring your own Anthropic or OpenAI key

Requirements

VS Code 1.90+, an Anthropic or OpenAI API key, and — for scaffolding — elan and lake. PDF import works too, with pdftotext or mutool, though .tex gives a materially better blueprint.

Built by meelgroup at Georgia Tech · Issues

Tex2Lean

kuldeepmeel

Tex2Lean

What you get

Quick start

Requirements