Contents

Lean beside a proof

Companion package

Lean beside a proof

A theorem, its proof and the Lean code that checks it can be shown together. The reader first sees the theorem. Two switches under its frame, Proof and Lean, open either or both below it: side by side on a wide screen, one under the other on a narrow one.

Theorem 1. The sum of the firstodd numbers is.

Proof. By induction on. Forboth sides are. If the sum of the firstodd numbers is, adding the next one gives

theorem sum_odd (n : β„•) :
    βˆ‘ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
  induction n with
  | zero => simp
  | succ k ih =>
    rw [Finset.sum_range_succ, ih]  -- peel off the last term
    ring
\begin{leantheorem}[decl=sum_odd]
\begin{theorem}
The sum of the first $n$ odd numbers is $n^2$.
\end{theorem}
\begin{proof}
By induction on $n$. For $n = 0$ both sides are $0$. If the sum of the
first $k$ odd numbers is $k^2$, adding the next one gives
\[ k^2 + (2k + 1) = (k + 1)^2 . \]
\end{proof}
\begin{leancode}
theorem sum_odd (n : β„•) :
    βˆ‘ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
  induction n with
  | zero => simp
  | succ k ih =>
    rw [Finset.sum_range_succ, ih]  -- peel off the last term
    ring
\end{leancode}
\end{leantheorem}

The environment leantheorem wraps an ordinary theorem, its proof and a leancode block; everything before \begin{proof} is the statement. The Lean code sits in a frame like the proof’s, in a colour of its own. It is not typeset: it is read verbatim, with its indentation, and shown as highlighted text that can be copied into an editor. Three keys set it up: decl= names the declaration above the code, url= makes that name a link (to its documentation, say), and show= sets what is open at first: none (the default here), proof, lean or both.

A proof on its own

When a proof is separated from its theorem, for example by a discussion, leanproof gives it the same switches, on a line of their own above it. It starts with the proof shown.

Proof. Both sides are the numeralonce the addition is carried out.

example : 2 + 2 = 4 := rfl
\begin{leanproof}[decl=two_add_two]
\begin{proof}
Both sides are the numeral $4$ once the addition is carried out.
\end{proof}
\begin{leancode}
example : 2 + 2 = 4 := rfl
\end{leancode}
\end{leanproof}

In print

A PDF shows the theorem and the proof as usual, followed by the code as a verbatim listing. The package option leanprint=false leaves the code out:

\usepackage[leanprint=false]{reflowtex}

Lean’s Unicode symbols (,,) need a monospaced font that has them, as with any listing: compile with LuaLA TEX and a font such as DejaVu Sans Mono (\setmonofont from fontspec).

Blueprints

Formalisation projects often describe their progress with Patrick Massot’s leanblueprint, whose macros tie a statement to a Lean declaration: \lean{Nat.sum_odd}, \leanok, \uses{thm:a,lem:b}, \proves{…}, \notready, \mathlibok. The package defines them, as markers with no output, when a document has not, so a blueprint’s sources compile here unchanged; leantheorem and leanproof then add the code itself wherever it should show.