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 .