Mathematics · proofs · software

The complete reading collection

Run Lean with its dependencies

Choose any of the 2,722 displayed source files. Prepare its imports, use a pinned Lean environment, and keep the actual compiler output.

This catalogue covers 20 reading editions: 1,462 files use retained projects and 1,260 use reconstructed workspaces. 0 need further setup. These are source selections, not theorem or successful-compilation counts.

Run on your computer

Download Lean runner · 20.5 MB

  1. Install Python 3.11+, Git, and Elan, Lean’s toolchain manager.
  2. Unzip the bundle and open a terminal in its folder.
  3. Choose a source above and run its command. Open RESULT.json and the logs in the new output folder.

Nothing runs when you browse this page. The downloaded runner executes native Lean on your computer. First runs can take several minutes and gigabytes of disk.

Two environments, stated explicitly

Retained project: use the original Lake configuration, Lean pin, lockfile, and local source modules.

Reconstructed workspace: keep the source bytes unchanged, collect its local imports, and use a fixed Lean/Mathlib environment. This is a new experiment rather than a replay of an absent project configuration. Ambiguous or missing imports stop preparation.

GitHub runs: repository maintainers can use the manual Lean source runner workflow. Paste the selected repository path into its source input. The job checks that file and saves its result and logs as an artifact.

Compiler errors, warnings, missing imports, and timeouts remain visible. A clean compiler exit does not audit axioms or establish that the entire paper is formalized. Existing coverage labels stay attached to their recorded evidence.

For interactive checking of custom modules inside this site, the runner can also export a project for a dedicated Lean web server. Backend setup and export instructions.

Environment catalogue and bundle checksum · Complete runner bundle