Paperproof: a proof history view for Lean 4 in VS Code

The idea is a proof history, not a proof viewer

Paperproof is described as a new proof interface for Lean 4, and the mechanism is stated in one sentence. It will inspect how the hypotheses and goals were changing throughout the Lean 4 proof, and display this history, making it equivalent to how we think of a mathematical proof on paper. That is the whole thesis, and it is a diagnosis as much as a feature. A Lean proof written in tactic mode is a sequence of state transformations, and the usual interface shows you the current state, so the intermediate steps, which is where a proof is actually constructed, exist only in your scrollback and in your memory. Paperproof reconstructs that sequence and lays it out as a tree, where each node is a step and the branches are the cases. The README's own example set makes the point, since the tables show what tactics such as apply, rw or cases look like in Paperproof and then render real proofs from well-known repositories. The project is MIT licensed, the site is paperproof.xyz, and the primary language is TypeScript.

The tactic table is the specification of what it handles

The first table in the README is the closest thing to a feature list, and it works by showing the Lean form and the Paperproof form side by side for each tactic. The cases covered are apply, have, intro, rw, by_contra, use, induction and cases, and the Lean snippets are the ones you would recognise from a textbook. A couple of them are more interesting than the rest. The induction example is written with an apostrophe, induction' n with k ih, and so is the cases example, cases' n with m, and the difference from the plain tactic names is the convention Lean uses for the versions that produce a proof term rather than a goal. The cases examples then show the three shapes that matter: a single inductive type, a conjunction with cases' h with a b, a disjunction with the same pattern, and a multi-constructor inductive where the pattern binds three names. The last of those is the case that shows what the tree is for, since a proof that branches three ways has a shape that a flat sequence of goal states does not communicate. The screenshots for the induction and cases rows are noticeably wider than the others, which is a small visual signal of the branching.

It renders proofs from real libraries, not toy examples

The second table drops the toy examples and points at three well-known sources. The first is Mathematics in Lean by Jeremy Avigad and Patrick Massot, taken from a solution file on infinitely many primes. The second is Mathlib, from the Power file in the algebra section. The third is the Hitchhiker's Guide to Logical Verification by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl and Jannis Limperg, from a functional programming demo file. Naming specific files at specific line numbers in three separate large projects is a much stronger claim than showing a proof you wrote for the README, because it says the tool handles the tactics and the notation that real mathematics libraries use, and that the rendering stays readable at the scale of a proof from a published textbook. The width of the rendered images is the other signal, with the Mathematics in Lean and Hitchhiker's Guide screenshots both being the full width of a proof page rather than the narrow single-step illustrations used for the tactics.

Installing it is a marketplace extension and one click

The installation is two steps, and the second one is telling you that you are done. You install the Paperproof VS Code extension from the marketplace, and then you click the Paperproof icon, which after installation should appear in all .lean files, and that opens a Paperproof panel within VS Code. The icon is described as appearing in all .lean files, so the extension attaches itself to Lean sources rather than to a project, which is convenient for anyone who works across several Lean repositories. There is one important limitation stated right after. You can click on any theorem now, well, only on tactic-based proofs, those starting with by, and you should see your proof tree rendered. So the extension is not a general Lean visualisation, it is a reader for the tactic mode of proof, which is where the state transitions are and therefore where the history is worth showing. A proof written entirely as a term, with no by block, has no tactic sequence to record.

How the project is built, and what is in the tree

The repository is a hybrid of a Lean package and a TypeScript application, and the top level shows the split. There is a lean/ directory holding the Lean side, an extension/ directory for the VS Code extension, an app/ directory, a paperproof.xyz/ directory for the website, and a _examples/ directory alongside an Examples.lean file at the top level. The build is driven by lakefile.lean with a lean-toolchain file, so the Lean side uses the standard Lake toolchain, and there is a Makefile for the rest. The extension target packages the extension with vsce into a vsix file, then uninstalls and reinstalls it into VS Code from the command line.

extension:
	cd extension && \
	vsce package --out paperproof.vsix && \
	code --uninstall-extension paperproof.paperproof || true && \
	code --install-extension paperproof.vsix

The comment above that target notes the manual step, that after the reinstall you have to close and open VS Code because that is hard to do programmatically. The website targets are separate, with a production target that builds the standalone rendered HTML with esbuild and deploys it via a shell script to a named host, and a local target that runs esbuild in watch mode alongside a local server. A .devcontainer/ directory is present, so a contributor can work in a container with the Lean toolchain already set up. The releases are v2.10.0 from 2026-04-08, v2.7.0 from 2025-11-16 and v2.4.0-lean from 2025-10-18, and the last push to the repository was on 2026-09-06.

Where Paperproof is the wrong choice

The first limit is scope, and it is the one the README states plainly. Only tactic-based proofs can be inspected, so a proof written as a term, or a file of definitions with no proof blocks, gets nothing from the extension, and the ecosystem around Lean has plenty of both. The second is that this is a presentation layer, not a prover. It reads what Lean already recorded and draws it differently, so it adds no checking and no confidence beyond what the elaborator gave you, and a tree diagram of a proof that does not compile is still a diagram of nothing. The third is the dependency on a specific editor. The extension lives in VS Code, and the build process itself shows the coupling, since packaging and reinstalling the extension is a Makefile target that shells out to the code command. A team working in Neovim, in an online Lean environment, or in a CI pipeline that wants a rendered proof artefact has no path from this repository. The fourth is that the project is young and moves quickly, with a version 2.4.0 tagged as lean in a way that suggests the packaging and the Lean version were being sorted out, and versions 2.7, 2.10 and others in between, which is a lot of churn for a tool people would want to rely on. And the fifth is the question of whether the goal widget is enough. For a reader who already knows Lean well, the state after each tactic is in the information panel and the history can be reconstructed. The value of Paperproof is highest for someone coming from paper proofs, or teaching, or reviewing a proof where the structure is the point rather than the individual steps.

Editorial conclusion

Adopt Paperproof if you write Lean 4 proofs and find the goal state after each tactic hard to reconstruct in your head, since the proof tree makes that history visible. Skip it if you already work fluently with the goal widget and the info view, since the extension is a different presentation of information Lean already shows, and skip it if your proofs are not tactic-based. Verify first that your Lean project uses the tactic style the extension reads, since the README notes that only tactic-based proofs starting with by can be clicked, and that the extension is installed from the VS Code marketplace.

Frequently asked questions

Official sources

1. License: MIT
2. Paper-Proof/paperproof on GitHub
3. Project website
4. README
5. Releases