Skip to main content
All modules

VerifierResearchmath

Lean Blueprint

A paper and its Lean 4 formalization kept in step. Every theorem links to a Lean declaration, the agent proves against the real compiler, and a status table shows exactly what is verified.

main.texLaTeX
\documentclass[11pt]{article}
\usepackage[margin=1in,marginparwidth=1.05in,marginparsep=10pt]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{blueprint}
\usepackage{hyperref}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}

\title{Sums of Odd Numbers\\[4pt]
  \large a tiny paper, kept in step with its Lean 4 proof}
\author{}
\date{\today}

\begin{document}
\maketitle

Each statement below names its Lean declaration with the \verb|\lean{...}|
macro; that name appears in the margin, and the margin gains a green check
the moment the Lean compiler accepts the declaration with no \texttt{sorry}.
The two lemmas are the leaves; the theorem \verb|\uses{...}| them, so its
proof depends on theirs. There is no Lean file yet: click \textbf{Formalize}
(next to Compile) and Sunny writes \texttt{main.lean}, proves the leaves
first (bottom up), then the theorem on top of them.

Write $S(n)$ for the sum of the first $n$ odd numbers,
$1 + 3 + \cdots + (2n-1)$.

% Leaf: true by definition. Close its `sorry` first.
\begin{lemma}\label{lem:sumodd-base}\lean{sumOdd\_zero}
$S(0) = 0$.
\end{lemma}

\begin{proof}
Immediate from the definition of $S$.
\end{proof}

% Leaf: the recurrence, also true by definition.
\begin{lemma}\label{lem:sumodd-step}\lean{sumOdd\_succ}
For every $n \in \mathbb{N}$, $S(n+1) = S(n) + (2n+1)$.
\end{lemma}

\begin{proof}
Immediate from the definition of $S$: the $(n+1)$-st odd number is $2n+1$.
\end{proof}

% Summit: depends on both leaves via \uses. It closes once they do.
\begin{theorem}\label{thm:odd-square}\lean{sumOdd\_eq\_sq}\uses{lem:sumodd-base,lem:sumodd-step}
For every $n \in \mathbb{N}$, the sum of the first $n$ odd numbers is $n^2$;
that is, $S(n) = n^2$.
\end{theorem}

\begin{proof}
Induction on $n$. The base case is Lemma~\ref{lem:sumodd-base}. For the step,
Lemma~\ref{lem:sumodd-step} gives
$S(n+1) = S(n) + (2n+1) = n^2 + 2n + 1 = (n+1)^2$.
\end{proof}

\end{document}

main.tex is a tiny paper: the sum of the first n odd numbers is n², built from two one-line lemmas (a base case and a recurrence). There is no Lean file yet, so the toolbar shows a Formalize button next to Compile. Click it (or say "formalize") and I'll install Lean in the sandbox (a few minutes once, instant after), write main.lean next to the paper, prove the two lemmas first, then the theorem that \uses{} them, and give each margin its green check. The theorem verifies only once both leaves do: that is the bottom-up shape you will watch fill in on the Lean graph. Nothing is marked verified until Lean accepts the real proof. Bring your own paper any time by pasting an Overleaf link or uploading a folder.

What’s inside

  • Skills
  • skills/lean-blueprint/SKILL.mdLean Blueprint · 5.2 KBKeeps main.tex and Formalization.lean in step. Use whenever the user asks to formalize a statement, prove a theorem, close a sorry, verify the paper, or whenever any theorem, lemma, or definition changes on either side. The workflow for the \lean / \leanok macros and status.md.
    ---
name: Lean Blueprint
description: >
  Keeps main.tex and Formalization.lean in step. Use whenever the user asks to
  formalize a statement, prove a theorem, close a sorry, verify the paper, or
  whenever any theorem, lemma, or definition changes on either side. The
  workflow for the \lean / \leanok macros and status.md.
---

# Lean Blueprint

One paper, two synchronized files. `main.tex` holds the mathematics for
humans; `Formalization.lean` holds the same statements for the Lean compiler.
This skill is the contract that keeps them in step.

## Setup (once per sandbox)

Run `bash setup.sh` with `timeout: 600` before any Lean command. The first
run installs the toolchain for a few minutes; reruns are a fast no-op. It also
installs `skills/lean4/SKILL.md`: read that skill for tactics, Mathlib search,
and decoding Lean's error messages. Compile with `lean Formalization.lean`.

## The linking convention (leanblueprint-compatible)

- Every formalized statement in `main.tex` carries `\lean{DeclName}` naming
  its Lean declaration (escape underscores in the argument: `\lean{foo\_bar}`).
  Multiple declarations for one statement are comma-separated.
- `\leanok` next to a statement means the compiler verified the linked
  declaration. It is EARNED, never decorative: add it only after the check
  below passes, and remove it the moment the declaration stops verifying.
- `\uses{labels}` records which blueprint statements a proof depends on.
- Each Lean declaration's doc comment names its LaTeX label
  (`Blueprint: Theorem `thm:...` in main.tex`), so the mapping is greppable
  from both sides.

## The verification check

`lean Formalization.lean` exiting 0 does NOT mean proved: `sorry` is only a
warning. The check that cannot be fooled is `#print axioms <name>`. If its
output contains `sorryAx`, the proof rests on a hole and the statement does
not get `\leanok`. Keep one `#print axioms` line per linked declaration at
the bottom of `Formalization.lean`, and add one for every declaration you add.

## The sync loop

After ANY of these: a statement edited in `main.tex`, a declaration edited in
`Formalization.lean`, a proof attempt, a new formalization,

1. Recompile `Formalization.lean` and read the real output.
2. Re-sync the other side. A changed LaTeX statement means the linked Lean
   statement must change to match, and vice versa. The two must assert the
   same mathematics: if you cannot make Lean state exactly what the paper
   states, say so; NEVER silently weaken or alter the claim in `main.tex` to
   make Lean accept it. Propose wording as a suggestion and let the user
   decide.
3. Update the badges: add or remove `\leanok` per the verification check.
4. Regenerate the table in `status.md`. Every theorem, lemma, and definition
   in `main.tex` gets a row; statuses are exactly one of `verified`,
   `statement verified, proof open (sorry)`, `broken (does not compile)`, or
   `not formalized`.
5. Report the compiler's real output to the user, including which proofs
   still rest on `sorry`.

## Formalizing a new statement

1. Read the LaTeX statement and its label.
2. Add the declaration to `Formalization.lean` with a doc comment naming the
   label. State first, prove second: a faithful statement with `sorry` beats
   a proved distortion.
3. Attempt the proof (see `skills/lean4/SKILL.md`). Leave `sorry` for what
   you cannot close, and never delete a `sorry` you did not close.
4. Add `\lean{...}` to the statement in `main.tex` (`\leanok` only if
   verified), add the `#print axioms` line, run the sync loop.

## Faithful statements

A statement counts as formalized only when the Lean declaration asserts the
paper's actual claim. Placeholder shapes — structure fields or hypotheses of
type `True`, props that elaborate but say nothing, simplified stand-ins —
are `not formalized` in `status.md`, however cleanly they compile. Before
marking any statement formalized, read the Lean declaration back into plain
mathematical prose WITHOUT looking at the LaTeX, then compare that prose
against the paper's statement; on any mismatch, fix the Lean or record
`not formalized` and say so. When the full statement needs machinery you
cannot state yet, keep the honest status and a note — never dress a stub up
as the theorem.

## Decomposition

When a full proof is out of reach, decomposition is the honest fallback,
never a bare give-up: reduce the sorry to named sub-lemmas — each its own
declaration ending `:= by sorry`, with a doc comment giving its plain-prose
statement and a marker comment `-- decomposed from: <parent declaration
name>` immediately above it — then prove the parent USING those sub-lemmas
so its own body is sorry-free. Sub-lemmas go in the same .lean file, before
the parent's source-line marker. A decomposed parent is "proved modulo N
open sub-lemmas" (its `#print axioms` still shows sorryAx), NEVER proved.
Never add sub-lemmas or any invented statement to the paper.

## Mathlib

Mathlib is prebuilt in the sandbox image: after `bash setup.sh`, plain
`lean` resolves `import Mathlib.*` against the baked cache in seconds.
Import it freely — real analysis, measure theory, geometry are all there.
Never run `lake new`, `lake cache get`, or compile Mathlib from source;
there is no lake project here and none is needed.
  • Starter files
  • main.texopens first · 1.9 KB
    \documentclass[11pt]{article}
\usepackage[margin=1in,marginparwidth=1.05in,marginparsep=10pt]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{blueprint}
\usepackage{hyperref}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}

\title{Sums of Odd Numbers\\[4pt]
  \large a tiny paper, kept in step with its Lean 4 proof}
\author{}
\date{\today}

\begin{document}
\maketitle

Each statement below names its Lean declaration with the \verb|\lean{...}|
macro; that name appears in the margin, and the margin gains a green check
the moment the Lean compiler accepts the declaration with no \texttt{sorry}.
The two lemmas are the leaves; the theorem \verb|\uses{...}| them, so its
proof depends on theirs. There is no Lean file yet: click \textbf{Formalize}
(next to Compile) and Sunny writes \texttt{main.lean}, proves the leaves
first (bottom up), then the theorem on top of them.

Write $S(n)$ for the sum of the first $n$ odd numbers,
$1 + 3 + \cdots + (2n-1)$.

% Leaf: true by definition. Close its `sorry` first.
\begin{lemma}\label{lem:sumodd-base}\lean{sumOdd\_zero}
$S(0) = 0$.
\end{lemma}

\begin{proof}
Immediate from the definition of $S$.
\end{proof}

% Leaf: the recurrence, also true by definition.
\begin{lemma}\label{lem:sumodd-step}\lean{sumOdd\_succ}
For every $n \in \mathbb{N}$, $S(n+1) = S(n) + (2n+1)$.
\end{lemma}

\begin{proof}
Immediate from the definition of $S$: the $(n+1)$-st odd number is $2n+1$.
\end{proof}

% Summit: depends on both leaves via \uses. It closes once they do.
\begin{theorem}\label{thm:odd-square}\lean{sumOdd\_eq\_sq}\uses{lem:sumodd-base,lem:sumodd-step}
For every $n \in \mathbb{N}$, the sum of the first $n$ odd numbers is $n^2$;
that is, $S(n) = n^2$.
\end{theorem}

\begin{proof}
Induction on $n$. The base case is Lemma~\ref{lem:sumodd-base}. For the step,
Lemma~\ref{lem:sumodd-step} gives
$S(n+1) = S(n) + (2n+1) = n^2 + 2n + 1 = (n+1)^2$.
\end{proof}

\end{document}
  • Libraries and docs
  • blueprint.sty965 B
    % Print-side subset of the leanblueprint macro convention
% (https://github.com/PatrickMassot/leanblueprint): \lean{} names the Lean
% declaration a statement is formalized as, \leanok marks it compiler-verified,
% \uses{} records dependency edges. Rendered here as margin badges so the PDF
% shows formalization status next to each statement.
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{blueprint}[2026/08/26 LaTeX-Lean blueprint status badges]
\RequirePackage{xcolor}
\RequirePackage{amssymb}

\definecolor{bpverified}{HTML}{1A7F37}
\definecolor{bpname}{HTML}{57606A}

% The Lean declaration(s) this statement is formalized as.
\newcommand{\lean}[1]{\marginpar{\raggedright\scriptsize\ttfamily\color{bpname}#1}}
% The compiler accepts the linked declaration with no sorry.
\newcommand{\leanok}{\marginpar{\raggedright\scriptsize\color{bpverified}\checkmark~verified}}
% Dependency edges between blueprint statements; metadata only in print.
\newcommand{\uses}[1]{}
  • FAQ-Lean.md6.9 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 `Hello.lean`; 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. Say **"go"** in the chat and the agent sets everything up. The toolchain
usually installs itself in the background the moment the workspace is created,
so by the time you ask your first question it's often already there. The first
setup can take a few minutes once; after that it's instant, and it survives
between sessions.

## 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 `AGENTS.md`, `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?

- **`Hello.lean`** — the working document. It ships with one theorem left as
  `sorry` so you can immediately ask the agent to prove it and watch the
  whole loop.
- **`AGENTS.md`** — the operating rules above (the honesty contract). It sits
  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.
- **`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.
- First-ever toolchain install: up to a few minutes, once — normally hidden in
  the background before your first message.

## What about Mathlib?

Say **"add Mathlib"**. It's several gigabytes, fetched from a prebuilt cache
into the hidden build directory, so expect the one-time setup to take a while.
The agent will warn you before starting. Until then, everything in core Lean
and its standard library works out of the box.

## 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.1 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"

# "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"

# 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.
if [ -f /opt/mathlib/.leanpath ]; then
  cat > /usr/local/bin/lean <<EOF
#!/bin/sh
[ -n "\${LEAN_PATH:-}" ] || export LEAN_PATH="$(cat /opt/mathlib/.leanpath)"
exec "$HOME/.elan/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
  tcdir="$HOME/.elan/toolchains/$(printf '%s' "$installed" | sed -e 's/\//--/g' -e 's/:/---/g')"
  # 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"