Lean

SCRP has Lean 4 installed, together with its version manager elan and build tool lake.

Check Lean Availability

Lean is set up automatically on login: the cluster’s shared copy of Lean is linked into your home directory, so no download is needed and almost no disk space is used. Because the setup runs at login, if you had a terminal open from before Lean was installed, you will need to open a new one.

To check Lean’s version, open a terminal and check:

lean --version

You should see something like Lean (version 4.35.0, ...).

What is Lean, elan, lake?

Lean’s setup is a little unusual, so a quick tour of the pieces:

• Lean - the programming language and proof assistant itself.
• elan - a version manager for Lean. Think of it as a “phone book” that figures out which version of Lean to run and forwards your commands to the right one.
• lake - Lean’s build tool. It handles projects with multiple files and dependencies, and turns your code into runnable programs.
• Toolchain - a specific version of Lean, installed on your behalf. Projects can pin down which version they want.

The cluster provides a shared toolchain (Lean 4.35.0) in /opt/network/elan/, linked into ~/.elan in your home directory.

Using a Different Version

To use the latest stable release:

elan default stable

or a specific version:

elan default leanprover/lean4:v4.35.0

Check what you have with elan show.

Note: each version you install yourself is downloaded into your home directory and takes about 3GB. To free up space, remove versions you no longer need:

elan toolchain uninstall leanprover/lean4:v4.35.0

To switch back to the cluster’s centrally-managed version, run:

elan default leanprover/lean4:v4.35.0

Create a Lean Project

Create a project folder, initialize, and build:

mkdir myproject && cd myproject
lake init
lake build

lake init creates a starter project in the current folder:

• a lakefile.toml (describing the project)
• a lean-toolchain file (pinning the Lean version)
• some additional starter Lean files.

lake build compiles it and produces a runnable program, which you can run with:

./.lake/build/bin/myproject

A fresh project builds in a few seconds. The project is pinned to whatever Lean version was your default at lake init time; the cluster’s shared copy is 4.35.0.

A One-File Test without a Project

For quick experiments you can skip lake entirely. Put this in a file called hello.lean:

def main : IO Unit := IO.println "Hello from Lean on SCRP!"

Then run:

lean --run hello.lean

Using Mathlib and MathEconLib: the Shared Library Pool

If you are doing mathematics, you will want Mathlib, Lean’s giant library of mathematical definitions and proofs. Economists may further want MathEconLib, a formal foundation for economics built on top of Mathlib: game theory, mechanism design and auctions, choice and matching theory, and pricing.

A Mathlib-based project normally costs about 7.5GB of disk space and a long first build. To avoid both, the cluster keeps a shared library pool: one copy of Mathlib (and MathEconLib), fully pre-built, that your project can link to instead of downloading its own. The pool’s versions are pinned (Lean 4.35.0, Mathlib v4.35.0, and MathEconLib’s current release).

To start a new project using the pool, just create a folder and run:

mkdir myproject && cd myproject
lean-setup new            # MathEconLib project (includes Mathlib)
lake build

This scaffolds lakefile.toml, lean-toolchain, and a starter Myproject.lean (the library name is the folder name, capitalized: myproject → Myproject), then links the pool. For a Mathlib-only project, use lean-setup new mathlib.

If you already have a project with its own lakefile.toml, link it to the pool from inside the project folder:

lean-setup matheconlib   # if your project uses MathEconLib (includes Mathlib)
lean-setup mathlib       # if your project uses Mathlib only
lake build

That’s it: no lake update, no lake exe cache get, no downloads. Your project folder stays a few MB.

A few things to pay attention to:

• You still need your own lakefile.toml still needs the right [[require]] entries; the pool only replaces the downloaded copies of those libraries.
• Don’t run lake update in a pooled project—it needs write access to the shared folders and will fail; that is by design.

If you need a different version (for example, a Mathlib release newer than the pool’s), switch the project to its own copies and update normally:

lean-setup unlink     # remove the links
lake update            # fetch your own copies of the dependencies
lake exe cache get     # fetch pre-built Mathlib for your version
lake build

Note that Lean, Mathlib, and your project must all agree on the version. The pool matches the cluster’s shared Lean 4.35.0 toolchain.

From then on the project is fully independent—it just costs its own ~7.5GB. Both kinds of projects coexist fine on the cluster.

Using Your Own Copies (no pool)

If you prefer not to use the pool (or need different versions), the standard Lean workflow works as usual. Add the dependency to lakefile.toml—Mathlib:

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.35.0"

or MathEconLib (add it instead of Mathlib; it pins Mathlib itself):

[[require]]
name = "matheconlib"
git = "https://github.com/matheconlib/matheconlib"
rev = "main"

Pin the toolchain to the matching version:

echo "leanprover/lean4:v4.35.0" > lean-toolchain

Note: Mathlib moves quickly and its latest release may require a newer Lean than the cluster’s shared version—in that case, install the version it asks for (elan default leanprover/lean4:vX.Y.Z) and accept the one-time download. To find a Mathlib release matching a given Lean version, check the tags: a release named v4.35.0 is built for Lean 4.35.0.

Then fetch and build:

lake update
lake exe cache get
lake build

lake exe cache get downloads ready-made files so your machine does not have to compile the whole library itself. Even so, expect the first build to use a good chunk of memory and disk (about 7GB in .lake/)—this is a good moment to move to a compute node:

srun -c 4 --mem=8G lake build

A Complete Example: Optimal Posted Pricing

This example puts everything together: a project, a pinned toolchain, the shared library pool, and MathEconLib. It proves the classic result that a seller facing a buyer whose value is uniformly distributed on [0, 1] maximizes expected profit by posting the price 1/2.

Set up the project with the pool scaffold:

mkdir pricing && cd pricing
lean-setup new

This creates lakefile.toml (with the MathEconLib dependency and a Pricing library target), lean-toolchain, a starter Pricing.lean, and the pool links. (The library name is the folder name, capitalized: pricing → Pricing.)

Replace the contents of Pricing.lean with:

import MathEconLib

open MathEconLib ValueDistribution

/-! # Optimal posted pricing on SCRP

A seller with zero cost faces a buyer whose value `v` is uniformly
distributed on `[0, 1]`. At price `p`, the buyer buys exactly when
`p ≤ v`, so the probability of a sale is `1 - p` and expected profit is
`p * (1 - p)`, maximized at `p = 1/2`. MathEconLib proves this. -/

-- The candidate price: the midpoint formula with zero continuation value.
-- `uniformOptimalPrice a b c = max a (min b ((b + c) / 2))`.
example : uniformOptimalPrice 0 1 0 = 1 / 2 := by
  rw [uniformOptimalPrice_eq_peak 0 1 0 (by norm_num)]
  norm_num

-- The hard part, proved by the library: among ALL prices in [0, 1],
-- expected profit is maximized exactly at the candidate price.
-- (`IsMaxOn f s x` says `f x ≥ f y` for every `y` in `s`.)
example :
    IsMaxOn
      (fun price ↦
        (uniformInterval 0 1 (by norm_num)).sellerProfit
          (SingleParameterProblem.postedPriceProblem 0 1 price) 0 0)
      (Set.Icc 0 1) (uniformOptimalPrice 0 1 0) :=
  isMaxOn_sellerProfit_uniformInterval 0 1 (by norm_num) 0 0

Build:

lake build

The first build takes a few minutes while Lake verifies the pre-built library files; after that, rebuilds take seconds. When it finishes, Lean has machine-checked that posting 1/2 really is the profit-maximizing price: no hand-waving, just a certificate you can re-verify any time.

(Without the pool, run lake update, lake exe cache get, then lake build Pricing instead—see “Using Your Own Copies” above.)

Cheat Sheet

Command	What it does
lean --version	Check Lean works and which version you have
elan show	What versions are installed and which is default
elan default leanprover/lean4:vX.Y.Z	Set your default version (downloads if you don’t have it)
elan toolchain uninstall <name>	Free up disk space
lake init	Start a new project in the current folder
lake build	Compile the project you are in
./.lake/build/bin/<projectname>	Run the compiled program
lean --run hello.lean	Run a single file, no project needed
lean-setup matheconlib	Link a project to the shared MathEconLib pool
lean-setup mathlib	Link a project to the shared Mathlib pool
lean-setup new [mathlib]	Scaffold a new pooled project in an empty folder
lean-setup unlink	Remove pool links; lake update then makes your own copies
srun -c 4 --mem=8G lake build	Build on a compute node