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.


Save the following sample LaTeX file as test.tex:

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)

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.
\newfontfamily{\freeserif}{DejaVu Sans}
  • 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.