LeanTeX

LeanTeX lets you embed Lean 4 code snippets directly in LaTeX and render both Lean output and diagnostics inside your compiled PDF.

Installation

Before continuing, make sure you have all required tools installed (see the Requirements tab).

1) Clone

git clone https://github.com/rgrossharv/LeanTeX.git
cd LeanTeX

2) Install Python package

python3 -m pip install .

python3 -m pip install -e .

python3 -m pip install --upgrade pip setuptools wheel

3) Install TeX package files

leantex install-tex

Quick Start

\usepackage{leantex}

leantex build path/to/file.tex

leantex watch path/to/file.tex

PYTHONPATH=. python3 -m leantex build path/to/file.tex

LaTeX Usage

\begin{lean}[name=demo,show=both]
#check Nat.succ
\end{lean}

\usepackage[onefile]{leantex}
# or
\usepackage{leantexonefile}

Examples

Examples live in examples/minimal. Use the dedicated examples page to view source and output: open examples page.

• minimal.tex — small demo
• test4.tex — larger sample using Mathlib imports

Documentation

For full details, see the README.

LeanTeX Requirements

Before installing LeanTeX, make sure your machine has:

• Python 3.9+ (with pip)
• Lean 4 + Lake (for running and checking Lean snippets)
• A TeX distribution with latexmk, listings, tcolorbox, and comment
• Git (to clone the repository)

Optional but recommended for larger examples (such as test4.tex): run lake update and lake exe cache get in examples/minimal.

LeanTeX Examples

This page shows example source and rendered PDFs from examples/minimal.