LeanTeX is a small LaTeX tool for writing mathematical documents that include Lean 4 code. The current version, LeanTeX v2.5, is built around native minted blocks and separate Lean output.

The idea is simple: write the Lean source as normal highlighted LaTeX code, then ask LeanTeX to print the corresponding diagnostics, goals, or infoview-style state where they are useful in the PDF.

The older v1 and v2 branches remain available for documents that depend on the earlier interfaces.

Native minted first

\usepackage[onefile]{leantexv2}

\leantexconfig{natcheck}{infoview=lines:4}
\begin{minted}[label=natcheck]{lean}
#check Nat.succ
example : 1 + 1 = 2 := by decide
\end{minted}

\leantexoutput{natcheck}

For hidden output-only snippets, use \leantex[infoview=lines:3]{...}.