The papers · A local proof workspace

Edit a proof. Ask Lean.

Explore a published proof, change a step, and check it on your own device. The compiler runs inside this browser.

17 prepared workspaces across 10 reading editions.

First run: download the Lean compiler and libraries, up to 417 MiB. Smaller workspaces need less.

Allow a few minutes for the first load, plus time for proof checking. Downloaded files are reused when your browser can cache them.

Open another retained Lean file

Explore any of the 2,722 files already included in the reading collection. The browser opens its retained local dependencies too. 363 files have import routes using the available libraries. These routes still need an actual Lean check; version differences, missing tactics and runtime limits can cause errors.

Opening a retained file downloads a 20 MiB source bundle.

Find a retained Lean file Retained source file

Open this panel to browse the source collection.

Published workspace

File to edit

Browser import route and compatibility

These retained sources run in the pinned browser environment. An available import route does not establish that the proof passes here.

Browser version compatibility lemma included

Lean checks this extra lemma alongside the workspace's final file. It supplies a name used by the paper that the older browser compiler lacks. Selected checks of earlier files do not add it. The original source below is unchanged.

Download the compatibility lemma

Support syntax defined in this file (experimental)

Tracks new commands and scoped notation as Lean checks the file. Each run starts a fresh compiler and can use more memory. Asynchronous elaboration and early stopping commands are rejected.

Lean source

Check selected file runs that file and its local dependencies. Run workspace checks every file in the workspace.

Loading the published workspace…

Lean’s response

No checks yet.

Download and compiler activity

Versions, source and limits

This pilot uses Lean 4.33.0, compiler revision 62b6a2291302, and selected Mathlib modules from de3a9cf33016. The papers’ retained projects may use different versions. Results here are browser experiments and do not change the collection’s recorded verification.

Choose from 17 prepared workspaces, or open another retained file above. Each prepared workspace starts with the Mathlib modules its sources need. Edited imports can load more available modules. You can edit any file in a workspace. Required project files are compiled first, then the dependent file. Imports outside the compiler-matched library set produce an error. Compiler crashes and interrupted checks produce no successful result.

For sources importing Mathlib.Tactic, the browser first checks a clearly labelled compatibility module importing the available tactics. It adds no declarations or assumptions. It is a subset of the original umbrella; missing tactics remain errors. Original source downloads stay unchanged.

For local imports, a generated wrapper names and exports the module into the compiler’s temporary filesystem. Original downloads remain byte for byte identical to the retained sources. A clean result means Lean completed checking these files with no reported warnings; it is not an audit of axioms or an entire paper.

Compiler and library downloads: up to 417 MiB across all available libraries. Proofs using only Std need less. Large files come from pinned public GitHub assets and are checked against the download record. Proof text stays in this tab and is not sent to a proof service; save a copy before leaving.

Source checksums · Compiler download record · Open source credits