leanify — a LaTeX article checked by Lean

Version 0.3, 2026-11-06.

Leanify compiles an ordinary mathematical article, written in LaTeX, to the Lean proof assistant: every definition and theorem becomes a Lean statement checked by the kernel, and the proofs are checked sentence by sentence against the results they cite. The same source is typeset as the paper you submit.

The LaTeX package leanify.sty is the typesetting side:

• it loads the notation the Leanify grammar reads (mathtools, amssymb);
• with shell escape, inside a Lean project, it runs lake exe leanify check on every compile and reports the findings as LaTeX warnings at their lines;
• with the option status, it marks every labelled result in the margin with its verification status (checked, derived, partly checked, compiled, false);
• without options and without shell escape, it changes nothing in the typeset article, so the article compiles anywhere, e.g. on arXiv.

\usepackage{leanify}            % check as you compile
\usepackage[status]{leanify}    % and show the verification status
\usepackage[certify]{leanify}   % and build the certificate first

The package needs LaTeX 2022-06-01 or newer. Checking needs the Lean toolchain (lake on the PATH) and the Leanify Lean package; typesetting does not.

Documentation: leanify-doc.pdf, and the full documentation, tutorial and demo at https://corrram.github.io/leanify/. Source and issues: https://github.com/Corrram/leanify.

Licence

Copyright (C) 2026 Marcus Rockel. Released under the Apache License, Version 2.0 (https://www.apache.org/licenses/LICENSE-2.0).