Overview
In this release, Paperproof makes it possible to see Lean code as LaTeX!
Screencast.from.2026-04-05.03-01-04.webm
Added
-
Display any Lean proof in LaTeX
The conversion is done using an LLM - counterintuitively, we found it more robust than encoding Lean-to-LaTeX mappings for any possible Lean syntax. We let the users add their own prompts to specify how exactly they'd like to latexify their proof.Lean LaTeX 
-
Added font-size increase/decrease
This lets you increase/decrease the font of goals and hypotheses.
Fixed
-
Lean versioning fixed
From now on, your Lean version won't be getting automatically increased upon Paperproof import unless it's absolutely necessary (we didn't know Lean does that, sorry!).
If you'd like to stay on the older version of Lean than the current Paperproof supports (at the moment of writing, Paperproof supports any Lean version ≥ v4.27.0), we wrote up VERSIONS.md that explains how to do it. -
Fixed "PANIC at List.head!" error
Paperproof was raising this error from time to time with no stack trace. That's fixed now.