New on CTAN: leanify
leanify: a LaTeX article checked by the Lean proof assistant. Leanify compiles an ordinary mathematical article, written in LaTeX, to Lean: every definition and claim becomes a kernel-checked Lean statement, and the proofs are checked sentence by sentence against the results they cite. The package leanify is the typesetting side: it checks the article as it compiles (with shell escape, inside a Lean project), reports the findings as LaTeX warnings at their lines, and with the option status marks every labelled result in the margin with its verification status. Without options it changes nothing in the typeset article.
This package is located at https://mirrors.ctan.org/macros/latex/contrib/leanify More information is at https://ctan.org/pkg/leanify
Thanks for the upload. For the CTAN Team Erik Braun CTAN is run entirely by volunteers and supported by TeX user groups. Please join a user group or donate to one, see https://ctan.org/lugs .
Leanify – A LaTeX article checked by the Lean proof assistant
This package connects mathematical articles written in LaTeX with the Leanify proof checker and the Lean proof assistant. It translates mathematical definitions, statements, and proofs supported by its grammar into Lean for formal verification. The same LaTeX source is used to typeset the article.
The leanify package provides the LaTeX integration. It loads
the required mathematical notation packages and, when shell escape is
enabled within a configured Lean project, invokes the checker during
compilation. Diagnostic messages are reported as LaTeX warnings at
the corresponding source lines. The status option displays
the verification status of labelled results in the margins.
Without shell escape, no external checker is invoked. Without options, the package leaves the typeset article unchanged. Thus, articles can also be compiled without the Lean toolchain, for example on arXiv. Formal verification requires the Lean toolchain and the separate Leanify checker.
| Paket | Leanify |
| Version | 0.3 |
| Copyright | 2026 Markus Rockel |
| Betreuer | Markus Rockel |