Offline proof presentation e.g. in PDF

Stream: Lean for teaching

[thielema]

I like to send a Lean4 proof of a mathematical problem to a mathematician who has no Lean installed. I thought it would be nice to have a tool, that converts a Lean4 proof to a kind of flip-book animation packaged in a PDF. That is, the PDF shall present the view of, say, VSCode, that is, the proof script on the left side and the current variables and goals on the right side. Landscape paper orientation would be prefered. Every PDF page highlights one proof step and shows the according outcome on the right side.
Is there already a tool that can do this?
Could be also nice for preserving proofs and may simplify upgrading them to future versions of Mathlib.

[Jannis Limperg]

Verso lets you generate websites and PDFs where you can see the proof states. Here's an example. (Ignore the ugly proof; it's AI-generated.) You might be able to get Verso to produce a document in your desired format by mashing together the verso-blog and verso-manual genres.

[Dan Velleman]

I made such displays in How To Prove It with Lean, especially in Chapter 3. However, I didn't have a tool to do it--I just created the displays by hand.

[Patrick Massot]

Unless you really really want a pdf rather than a web page then verso is definitely the way to go.

[Shreyas Srinivas]

Is there a verso tutorial in the style of markdown tutorials?