Leanify

One LaTeX source, read twice: typeset as the paper you submit, and compiled by Lean into kernel-checked statements and proofs.

Get started See the live demo

Leanify compiles an ordinary mathematical article, written in good mathematical English, to Lean. Every symbol must be defined in the article before it is used, every sentence has one fixed reading, and a proof step may use only the results it cites. The Lean kernel checks the compilation, every definition, every claim and every step of every compiled proof. There is no second, hand-written formal version that could drift away from the paper.

From a sentence to a theorem

The article

Define $f:(0,\infty)\to\mathbb{R}$ by
$f(x)\coloneqq x+\frac1x$.

\begin{theorem}\label{thm:bound}
For every $x\in(0,\infty)$, $f(x)\ge2$.
\end{theorem}

compiles to

def f : ℝ → ℝ := fun x => x + 1 / x

-- f is defined on (0,∞), where 1/x makes sense
def wellDefined0 : Prop := ∀ (x : ℝ), 0 < x → ¬x = 0

def claim2 : Prop := ∀ (x : ℝ), 0 < x → 2 ≤ f x

The theorem's proof compiles sentence by sentence, so Lean derives claim2 from exactly the steps of that proof and the lemma they cite, and each step from what it rests on. A draft that said $f(x)>2$ is refuted at x = 1, and the reader, the diagnostics and the margin of the PDF mark it false.

What you get

• Feedback while you write

  ---

  lake exe leanify check reads the article in about a second: undefined symbols, statements without a reading, and the formal reading of every claim.

• A certificate

  ---

  lake build has the kernel check every definition, claim and proof step. Certify while proofs are still sorry, and refute claims that are false as stated.

• The paper, unchanged

  ---

  The same .tex file typesets as before. \usepackage[status]{leanify} adds the status of every result in the margin.

• A reader for your readers

  ---

  A web page of the article with a marker at every sentence: its status, formal reading, Lean statement, premises and justification. Try it.

In three commands

lake exe leanify check Note/article.tex --claims   # what Leanify reads, in a second
lake exe leanify init Note/article.tex             # the Lean files, with a stub proof per claim
lake build Note.Certified                            # the kernel checks the article and your proofs

The tutorial takes a one-page note from a draft with four mistakes to a certificate, with the real output of every step.

Research articles

Two published articles are compiled from their LaTeX sources in lean-verifications:

• Rank weighting and asymmetry in Blest's rank correlation: two exact regions (arXiv:2609.27634): 37 definitions and 48 claims, all certified. The proof of Corollary 3.2 is checked sentence by sentence against what it cites. Source
• The exact region determined by Spearman's rho and Gini's gamma (arXiv:2609.19890): 11 definitions and 8 claims, all certified. Source

What the grammar reads today, and what comes next, is in Status and roadmap.