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.

Download the contents of this package in one zip archive (277.9k).