VerifierProjectsmathcs

Lean 4

A Lean 4 proving workspace. Lean and Mathlib come ready in the sandbox; one setup command links them and adds the community lean4-skills pack, and Hello.lean is a one-file example to build on.

Hello.leanLean 4

/-
Run this file with `lean Hello.lean`.
(If `lean` is not found, run `bash setup.sh` first.)
-/

def greeting : String := "Hello from Lean 4"

#eval greeting

/-- `sorry` means "trust me for now": the file still compiles, but this is not
    proved. Ask the agent to fill it in. -/
theorem add_comm' (a b : Nat) : a + b = b + a := by
  sorry

-- Prints `sorryAx` while the hole is there, and nothing once it is closed.
-- This is the honest check: `lean` exits 0 either way.
#print axioms add_comm'

This is a Lean 4 workspace. Lean and Mathlib are already on my computer, so say "go" and I'll get going right away. Hello.lean has one theorem left as sorry. Ask me to fill it and the proof arrives as a tracked edit you can review.

What’s inside

Starter files

Hello.leanopens first · 500 B

/-
Run this file with `lean Hello.lean`.
(If `lean` is not found, run `bash setup.sh` first.)
-/

def greeting : String := "Hello from Lean 4"

#eval greeting

/-- `sorry` means "trust me for now": the file still compiles, but this is not
    proved. Ask the agent to fill it in. -/
theorem add_comm' (a b : Nat) : a + b = b + a := by
  sorry

-- Prints `sorryAx` while the hole is there, and nothing once it is closed.
-- This is the honest check: `lean` exits 0 either way.
#print axioms add_comm'

Libraries and docs

FAQ-Lean.md7.1 KBShared lean4-setup bundle.

# Lean 4 workspace — FAQ

Short answers to the questions everyone asks in their first session. The
document you write proofs in is a `.lean` file; everything else here explains
what happens around it.

## What is this workspace?

A Lean 4 proving workspace. You (and Sunny, the agent) write theorems in
`.lean` documents, and a real compiler checks every proof. Nothing is "proved"
by assertion here: a claim counts only when Lean accepts it.

## Do I need to install anything?

No. Lean and Mathlib come already installed on Sunny's computer, so there is
nothing to download. After a break of 15 minutes or more, Sunny's computer
takes a short moment to start again.

## Where does compilation actually happen?

In a cloud sandbox attached to this workspace: a headless Linux machine where
the agent runs `lean` on your files. There is also a separate warm "prover
pool" that can check a file in a couple of seconds without touching the
sandbox. Both engines are infrastructure, not content — which is why you
don't see them in your file tree.

## Why can't I see Lean itself in my files?

Deliberate. The ~1 GB toolchain (and any build trees like `.lake/`) live in
hidden directories that the workspace mirror ignores. Your file tree shows
*documents* — the mathematics — never the machinery. If the tree ever filled
with thousands of toolchain files, something would be wrong.

## Is the `.lean` document the input or the output?

It's the **source, and the only durable artifact** — the same role a `.tex`
file plays for a paper. The compiler reads it and emits diagnostics; those
diagnostics are transient text, not a file. So:

- **Input:** your `.lean` documents (plus the workspace rules, `skills/`, `setup.sh`).
- **Output that persists:** the proof itself, written into the `.lean` document
  as a tracked, attributed edit.
- **Output that doesn't:** compiler messages. They surface in the chat — raw
  terminal output inside the expandable tool call, and the agent's summary in
  prose. Unlike LaTeX (which produces a `main.pdf` you can open), Lean's
  output is only ever diagnostics, so it lives in the conversation, not the
  tree.

## Why is it called `sorry`?

It's Lean's own keyword, not ours — a placeholder you write where a proof
should go, and the compiler accepts the theorem without one. The name is
old proof-assistant humor (inherited from Isabelle): you're apologizing for
the missing proof. The community speaks in it — "close the sorry",
"sorry-free" — and the compiler prints it verbatim, so we use the standard
word. Coq says `Admitted` for the same idea.

## How do I know a proof is real?

`lean` exits successfully even when a proof still contains `sorry` — the
placeholder for "trust me" — so a green run proves nothing by itself. The
check that cannot be fooled is `#print axioms <theorem>`: if `sorryAx`
appears, the proof rests on a hole. The agent is bound by this workspace's
rules to run that check and report the compiler's real output, never to
delete a `sorry` it didn't close, and never to weaken a statement to get
past one.

## What happens when I click Formalize?

A whole campaign starts, and it runs as a sequence of separate agent turns,
each in its own chat you can open and read. One turn translates every
statement in the paper into a Lean declaration beside it. Then a fresh reader
that has never seen your paper reads the Lean back into plain prose and fixes
any statement that turns out to say something different from your text. Then
proving runs, one statement at a time, always picking one whose ingredients
are already proved. At the end another blind reader audits the finished Lean
against the paper and files a verdict for every statement. (Formalize appears
only when there is a paper to formalize, so a plain Lean workspace with no
`.tex` never shows it.)

## Does it keep going on its own? What stops it?

It keeps going on its own, and the loop belongs to the platform rather than to
the agent. Each turn does one job and ends with a report; the system then
checks the file with the compiler and decides what runs next. Three things
finish a campaign: everything is proved, three rounds pass with no progress,
or the round cap is reached. In all three the audit runs before it ends, so
you always get the verdicts for what was done. Stopping a run yourself is the
one exception: that ends the campaign where it stands, and pressing Formalize
again starts a fresh one from the current state of the files.

## Who decides that a statement is proved?

The compiler, never the model. After each turn the platform runs your file on
the prover pool and reads `#print axioms` for every declaration, so a
statement counts as proved only when Lean accepts a proof with no holes. What
the agent says about its own work is a report, not a verdict. Lost work is
picked up too: if a turn crashes or its result never arrives, a background
check notices within about a minute and runs it again instead of leaving the
campaign stalled.

## What are all these starter files for?

- **Your `.lean` document** — the working file, and which one you start with
  depends on how the workspace arrived. A plain Lean workspace ships
  `Hello.lean`, one theorem left as `sorry`, so you can immediately ask the
  agent to prove it and watch the whole loop. A blueprint workspace starts
  from the paper instead: the statements live in `main.tex`, `blueprint.sty`
  defines the macros that link each one to a declaration, and the Lean file is
  written beside the paper the first time you click Formalize. So if you are
  looking for a Lean file to run and cannot find one, you are in the second
  kind: press Formalize and it appears.
- **The workspace rules** — the honesty contract above, kept as a file at the
  root because that's where every agent looks: Sunny reads it, and so do
  Claude Code or Codex if you sync this workspace to a folder. A blueprint
  workspace keeps them in its `skills/` entry; a plain Lean workspace gives
  them to Sunny directly.
- **`skills/`** — reference material on tactics, Mathlib style, and error
  repair. Agents load only the piece they need, when they need it. The
  root-level `skills/` layout is the open cross-agent standard, so any agent
  you bring benefits.
- **`setup.sh`** — the environment bootstrap, kept as a readable file so you
  can see exactly what gets installed. Re-running it is always safe.

## How fast is everything?

- A proof check on the warm pool: a couple of seconds.
- A typical agent turn (edit the proof, verify, report): one to a few minutes,
  dominated by the model's thinking, not the compiler.
- Sunny's computer starting after a break: a short wait, usually done in the
  background before your first message.

## What about Mathlib?

It's already there. Sunny's computer ships with Mathlib prebuilt, so
`import Mathlib` works with no download and no wait.

## What is this good for?

- A paper and its machine-checked proofs in one place: the theorem statement
  in `main.tex`, the Lean twin beside it, every claim compiler-verified.
- Fill-the-`sorry` teaching and coursework, with grading that can't be fooled.
- Formalization work against Mathlib.
- Pair it with the Math Research assistant: find the theorem in the
  literature, then formalize it here.

Sandbox setup

setup.sh9.8 KBRuns as bash setup.sh when the workspace opens.

#!/usr/bin/env bash
#
# Installs Lean 4 (latest stable) and the lean4 skill into this workspace's
# sandbox. Run it with `bash setup.sh`. Re-running it is a fast no-op.
set -euo pipefail

# Work from the workspace root. A workspace that combines templates seeds this
# file under `lean4/`, and only a root-level `skills/` tree is one the agent
# can see.
cd "${WORKSPACE_DIR:-$PWD}"
HOME="${HOME:-/root}"

# Belt-and-suspenders serialization for callers outside the file server. The
# server itself prioritizes an interactive chat command over its create-time
# warmup and retries the idempotent warmup after the interactive queue drains.
mkdir -p .sundial
exec 9>".sundial/setup.lock"
flock 9

# The toolchain is ~1GB, so it lives under .sundial/ — the one directory on the
# workspace volume that the doc-store mirror ignores. It survives an idle-down
# there instead of becoming a thousand workspace documents. $HOME/.elan points
# at it, which is where elan and its shims look with no configuration.
mkdir -p .sundial/elan
ln -sfn "$PWD/.sundial/elan" "$HOME/.elan"

# Repair what an older setup.sh broke: it wrote its Mathlib `lean` wrapper
# THROUGH the shim link, over elan itself, and every elan call then looped.
# The real elan is a binary, never that script; drop a clobbered copy (on
# the volume it outlives the container) so the link step below restores it.
for f in "$HOME"/.elan/bin/*; do
  { [ "$(head -c 2 "$f" 2>/dev/null)" = '#!' ] && grep -qs LEAN_PATH "$f" && rm -f "$f"; } || true
done

# "Installed" means the toolchain RUNS. Asking elan (never probing through the
# shims: with a channel-name default they resolve "stable" over the network on
# every call) and executing lean by its CONCRETE toolchain name catches every
# way a cancelled first run can die: elan missing, toolchain missing, and a
# kill mid-extract that left a dir elan believes is installed.
installed="$("$HOME/.elan/bin/elan" toolchain list 2>/dev/null | grep lean4 | head -n1 | awk '{print $1}' || true)"
if [ -z "$installed" ] || ! "$HOME/.elan/bin/elan" run "$installed" lean --version >/dev/null 2>&1; then
  # Fast path: link toolchains instead of downloading them. Two sources, in
  # preference order:
  #   /opt/lean-toolchains — baked into the sandbox IMAGE. Modal serves image
  #     layers from worker-local cache, so reads are fast even in a fresh
  #     container. This is the instant path.
  #   /opt/toolchains — the shared read-only volume (seeded by the Lean
  #     pool), the update lane for versions added between image rebuilds.
  #     Network-backed, so first reads are slower (the prewarm below covers
  #     them).
  # Linked under the fully-qualified name (decoded from elan's dir encoding:
  # -- => /, --- => :) so no shim call ever re-resolves a channel over the
  # network.
  for SRC in /opt/lean-toolchains /opt/toolchains; do
    [ -x "$SRC/lean-bin/elan" ] && [ -d "$SRC/lean" ] || continue
    echo "==> Linking Lean 4 from $SRC"
    # Probe by RUNNING elan, never by existence: a cancelled copy can leave a
    # partial binary that exists but cannot execute, and an existence guard
    # would skip the repair forever.
    if ! "$HOME/.elan/bin/elan" --version >/dev/null 2>&1; then
      mkdir -p "$HOME/.elan/bin"
      # The shims (lean, lake, ...) are all the elan binary dispatching on
      # argv[0]; copy it once and symlink the rest instead of copying ~10MB
      # per shim.
      cp -f "$SRC/lean-bin/elan" "$HOME/.elan/bin/elan"
      for shim in "$SRC"/lean-bin/*; do
        base="$(basename "$shim")"
        [ "$base" = "elan" ] || ln -sf "$HOME/.elan/bin/elan" "$HOME/.elan/bin/$base"
      done
    fi
    for dir in "$SRC"/lean/*/; do
      [ -d "$dir" ] || continue
      dir="${dir%/}"
      name="$(basename "$dir" | sed -e 's/---/:/g' -e 's/--/\//g')"
      # First source wins for a given version: skip names already linked.
      [ -e "$HOME/.elan/toolchains/$(basename "$dir")" ] && continue
      "$HOME/.elan/bin/elan" toolchain link "$name" "$dir" >/dev/null 2>&1 || true
    done
  done
  # Default to an image-resident toolchain when there is one — it is the
  # fast-read source — falling back to whatever got linked or installed.
  imgdir="$(ls -d /opt/lean-toolchains/lean/*/ 2>/dev/null | head -n1 || true)"
  if [ -n "$imgdir" ]; then
    installed="$(basename "${imgdir%/}" | sed -e 's/---/:/g' -e 's/--/\//g')"
  else
    installed="$("$HOME/.elan/bin/elan" toolchain list 2>/dev/null | grep lean4 | head -n1 | awk '{print $1}' || true)"
  fi
fi
if [ -z "$installed" ] || ! "$HOME/.elan/bin/elan" run "$installed" lean --version >/dev/null 2>&1; then
  echo "==> Installing Lean 4 (latest stable)"
  if [ -x "$HOME/.elan/bin/elan" ]; then
    # elan survived a cancelled run; drop any partial toolchain and refetch.
    [ -n "$installed" ] && "$HOME/.elan/bin/elan" toolchain uninstall "$installed" || true
    "$HOME/.elan/bin/elan" toolchain install stable
    installed="$("$HOME/.elan/bin/elan" toolchain list 2>/dev/null | grep lean4 | head -n1 | awk '{print $1}' || true)"
  else
    # --default-toolchain none: the installer's own toolchain download is not
    # reliable — observed live setting the default without fetching anything,
    # which fed the pin step below an empty name. Install explicitly instead.
    curl -sSfL https://elan.lean-lang.org/elan-init.sh \
      | sh -s -- -y --no-modify-path --default-toolchain none
    "$HOME/.elan/bin/elan" toolchain install stable
    installed="$("$HOME/.elan/bin/elan" toolchain list 2>/dev/null | grep lean4 | head -n1 | awk '{print $1}' || true)"
  fi
fi

if [ -z "$installed" ]; then
  echo "error: no Lean toolchain after install; run 'elan toolchain install stable' and re-run setup.sh" >&2
  exit 1
fi

# Pin the default to that concrete version. Left as the channel name
# ("stable"), every shim call re-resolves it against GitHub — a network round
# trip per lean invocation (measured 2.2s vs 0.04s pinned), a hang when the
# API stalls, and a surprise re-download the day a new release lands.
"$HOME/.elan/bin/elan" default "$installed"
tcdir="$HOME/.elan/toolchains/$(printf '%s' "$installed" | sed -e 's/\//--/g' -e 's/:/---/g')"

# Every bash call is a fresh shell, so PATH has to be permanent. /usr/local/bin
# is already on it, and empties on reboot while the volume does not — so relink
# every run.
ln -sf "$HOME"/.elan/bin/* /usr/local/bin/

# Mathlib is baked into the sandbox image: /opt/mathlib holds a full checkout
# with its built olean cache, and /opt/mathlib/.leanpath is the search path
# that lets plain `lean` resolve `import Mathlib.*` against it (the image's
# default toolchain is Mathlib's own pin, so the oleans are coherent). Env
# vars don't survive between bash calls, so bake the path into a wrapper —
# written after the relink above so every rerun restores it. Drop the link
# first: writing through it overwrote elan itself (the shims are hard links
# of it), and a wrapper that execs the shim execs itself forever. It execs
# the toolchain's own binary instead.
if [ -f /opt/mathlib/.leanpath ]; then
  rm -f /usr/local/bin/lean
  cat > /usr/local/bin/lean <<EOF
#!/bin/sh
[ -n "\${LEAN_PATH:-}" ] || export LEAN_PATH="$(cat /opt/mathlib/.leanpath)"
exec "$tcdir/bin/lean" "\$@"
EOF
  chmod +x /usr/local/bin/lean
fi
lean --version

if [ -f skills/lean4/SKILL.md ]; then
  echo "==> lean4 skill already installed (rm -rf skills/lean4 to refresh)"
else
  echo "==> Installing the lean4 skill"
  # Run the CLI from a staging dir under .sundial/ (mirror-ignored): its output
  # is cwd-relative, and alongside the per-agent install dir it drops a
  # skills-lock.json — at the workspace root that would mirror into a workspace
  # document and a diff card of its own. The agent reads skills from `skills/`,
  # so stage the copy in .sundial/ too and rename it into place: an interrupted
  # run can then never leave a partial skills/lean4 for the SKILL.md gate above
  # to mistake for installed, and a rerun can't nest into skills/lean4/lean4.
  rm -rf .sundial/skills-cli && mkdir -p .sundial/skills-cli
  (cd .sundial/skills-cli && npx -y skills@latest add cameronfreer/lean4-skills --skill lean4 --agent claude-code --yes)
  rm -rf .sundial/lean4-skill.tmp skills/lean4
  cp -RL .sundial/skills-cli/.claude/skills/lean4 .sundial/lean4-skill.tmp
  mkdir -p skills
  mv .sundial/lean4-skill.tmp skills/lean4
fi

# Prewarm: fault the toolchain + core oleans into THIS container's cache.
# The toolchain lives on a network-backed volume (shared or workspace), so a
# fresh sandbox's first real `lean` otherwise pays minutes of COLD RANDOM
# reads. Stream the whole toolchain dir sequentially first: measured on the
# shared volume, tar-reading 2.9GB cold takes ~2s where the same bytes as
# random compile-time faults took 4m18s. Near-instant when the cache is
# already warm, which is also why this runs on every no-op rerun. `h` follows
# the symlinks a linked toolchain resolves through.
# The page cache is per-container, so a container-local sentinel is exactly
# the right scope: the second setup run in the same container (warmup racing
# a chat turn) must not redo a multi-minute stream that bought it nothing
# (measured: 77s of pure waste on the go-turn).
echo "==> Warming the Lean cache"
SENTINEL=/tmp/.sundial-lean-prewarmed
if [ -e "$SENTINEL" ]; then
  echo "    cache already warmed in this container"
else
  # Image-resident toolchains skip the stream: Modal image reads are served
  # from worker cache and don't need sequential prefaulting. Only stream when
  # the active toolchain resolves to the network-backed volume.
  case "$(readlink -f "$tcdir" 2>/dev/null || echo "$tcdir")" in
    /opt/lean-toolchains/*) ;;
    *) [ -e "$tcdir" ] && tar chf /dev/null -C "$tcdir" . 2>/dev/null || true ;;
  esac
  printf 'example : True := .intro\n' > .sundial/warm.lean
  lean .sundial/warm.lean
  rm -f .sundial/warm.lean
  touch "$SENTINEL"
fi

echo "==> Ready. Try: lean Hello.lean"