Markus Rockel submitted the

leanify

package.

Version: 0.3 License: apache2

Summary description: A LaTeX article checked by the Lean proof assistant

Announcement text: --------------------------------------------------------------------------------

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 .