The Pygments syntax highlighting library has official support for Lean (however, Lean 4 keywords have not been added yet), which can be used in LaTeX via the minted package.

# Example

Save the following sample LaTeX file as test.tex:

\documentclass{article}
\usepackage{minted}
\usepackage{fontspec}
\setmainfont{FreeSerif}
\setmonofont{FreeMono}
\usepackage{fullpage}
\begin{document}
\begin{minted}[mathescape,
linenos,
numbersep=5pt,
frame=lines,
framesep=2mm]{Lean}
theorem mul_cancel_left_or {a b c : ℤ} (H : a * b = a * c) : a = 0 ∨ b = c :=
have H2 : a * (b - c) = 0, by simp,
have H3 : a = 0 ∨ b - c = 0, from mul_eq_zero H2,
or.imp_or_right H3 (assume H4 : b - c = 0, sub_eq_zero H4)
\end{minted}
\end{document}


You can compile test.tex by executing the following command:

xelatex --shell-escape test


Some remarks:

• either xelatex or lualatex is required to handle Unicode characters in the code.
• --shell-escape is needed to allow xelatex to execute pygmentize in a shell.
• If the chosen monospace font is missing some Unicode symbols, you can direct them to be displayed using a fallback font or other replacement LaTeX code.
\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{✝}{\freeserif{✝}}
\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}

• minted has a "helpful" feature that draws red boxes around characters the chosen lexer doesn't recognize. Since the Lean lexer cannot encompass all user-defined syntax, it is advisable to work around this feature.