How this site is verified

Every theorem you have read on this site was proved by the Lean compiler, not asserted by the author. This page is the mechanism behind that claim: the toolchain, what CI actually checks, how a snippet gets from lean/ onto a page, and how to run every step yourself.

The toolchain and the Mathlib pin

lean/lean-toolchain pins Lean at leanprover/lean4:v4.34.0-rc2. lean/lakefile.toml pins Mathlib at commit 3a8a89422e16d67b7ae57698f6d96e389e4d4202. These two numbers are not arbitrary: the public playground at live.lean-lang.org serves a project called MathlibDemo, advertised as “Latest Mathlib with Lean v4.34.0-rc2”, and that project’s own lean-toolchain and committed lake-manifest.json are exactly this Lean version and this Mathlib commit. Matching them buys two things: a runnable “Run in playground” button whose code compiles in the same environment lean/ was compiled in, and a lake exe cache get that pulls already-built .olean files instead of compiling Mathlib from source.

lake build

cd lean
lake build

lakefile.toml sets globs = ["MrCLean.+"], so this compiles every file under lean/MrCLean/, not only the ones reachable by import from MrCLean.lean. That matters because the chapter snippet source files (e.g. MrCLean/Fundamentals/Ch02Tactics.lean, MrCLean/Chapters/Ch08Unbiasedness.lean) are quoted by the website but imported by nothing — without the glob they could go stale silently. With it, a broken chapter snippet fails CI exactly like a broken library file.

axiom-audit and #print axioms

lake build on its own only warns about an incomplete proof — a sorry does not fail the build by itself. What actually forbids sorry is the axiom-audit step in .github/workflows/lean.yml (leanprover/lean-action@v1, axiom-audit: true, axiom-audit-allow: "propext,Classical.choice,Quot.sound", axiom-audit-root: "MrCLean"): it walks every declaration under the MrCLean namespace, follows its proof term’s transitive dependencies, and fails the job if anything reaches an axiom outside that allowlist. sorry is not a silent gap in the kernel’s bookkeeping — it is an axiom, sorryAx, and a proof that uses it anywhere in its dependency graph is caught here.

#print axioms <name> is the same walk, run by hand on one declaration — the tool to reach for when reading someone else’s formalization, including your own drafts. It guarantees the proof term is honest: no hidden sorry, no exotic axiom. It guarantees nothing about the statement — a theorem with an unsatisfiable hypothesis, or the wrong quantifier order, can be completely axiom-clean and still worthless. See the “Reading autoformalized Lean” section of any chapter for that half of the checklist.

Snippet markers and how the site lifts code from lean/

Chapters never retype library Lean. A file under lean/ marks a region with ordinary line comments:

-- SNIPPET: ht-unbiased
theorem HT_unbiased (D : Design n) (P : Population n) … := by
  -- SOLUTION
  rw [hexpand, …]
  ring
  -- END SOLUTION
-- END SNIPPET

and an MDX chapter reaches for it with <Snippet file="MrCLean/Estimators.lean" name="ht-unbiased" />. getSnippet (src/lib/snippets.ts) reads the file at Astro build time — not at request time, not in the browser — extracts the named region, and returns solution (the region as written), exercise (each -- SOLUTION block replaced by sorry), and a preamble the region needs to compile standalone. A missing file or a misspelt region name throws, which fails npm run build: a page that promises machine-checked proofs cannot silently render an empty code block.

The three preamble routes

A playground buffer can only import Mathlib — it has no access to this repository — so whatever a snippet depends on has to travel with it. In order of priority:

1. An explicit preamble region. A self-contained chapter file declares -- SNIPPET: preamble … -- END SNIPPET and it is used verbatim.
2. Inlining the library. A file that imports MrCLean.Core cannot say that to the playground, so the preamble is synthesized: import Mathlib plus any other non-local import, hoisted to the top; every MrCLean.* module in the file’s transitive import closure, in dependency order, with its own imports stripped; then everything in the snippet’s own file that precedes the region.
3. Neither. The file’s own header (imports, opens) plus whatever precedes the region.

Routes 2 and 3 always end with a loud separator comment —

/- ═══════════════════════════════════════════════════════════════════════
   The exercise is below this line. Everything above is the MrCLean library,
   compiled by CI; scroll past it.
   ═══════════════════════════════════════════════════════════════════════ -/

— because a derived preamble always contains code the reader never asked to see; a self-contained page has nothing to scroll past. LeanBlock prints a note next to the run button whenever the preamble exceeds 40 lines, which is most of them: the inlined library preamble typically runs 1,000–1,900 lines and elaborates in a few seconds in the reader’s browser.

npm run snippets:check

lake build proves the files under lean/ compile as a library — imports resolved by the module system, namespaces intact. It says nothing about whether the flattened, self-contained buffer a reader actually receives also compiles: imports hoisted, modules concatenated, namespaces cut wherever the region starts. scripts/check-snippets.mjs closes that gap: for every -- SNIPPET: region under lean/, it generates the exact buffer the playground would get and runs lake env lean on it directly (never lake build, so it is safe to run concurrently with someone else’s lake build). The solution form must compile with no errors and no warnings; the exercise form may warn only about the sorry it intentionally contains. A file whose markers don’t parse is reported as a failure, not silently skipped.

npm run snippets:check                     # every region under lean/
make lean-snippets-check FILE=MrCLean/Blocking.lean NAME=blocked-unbiased
make snippets-preambles                    # list sizes and inlined modules only

It runs at roughly ten seconds per region, so it is not part of npm run build — CI runs it as its own step, after lake build.

CI workflows

.github/workflows/lean.yml — every push and pull request. Installs elan, restores the Mathlib build cache, runs lake build with the axiom audit, then concatenates the five core library files after a single import Mathlib and compiles that (the same self-contained-unit check the snippet system does, run once over the whole core), then npm run snippets:check over every region.

.github/workflows/deploy.yml — pushes to main, or manual dispatch. Runs npm test (playground URL round-trips, snippet extraction, import closures) and npm run check (astro check, zero errors), builds the site, and deploys dist/ with wrangler pages deploy --project-name=mrclean.

Neither workflow currently blocks the other: the Lean library and the site can each be broken independently, and each workflow reports that independently. A green deploy.yml says the site builds and its own tests pass; it does not by itself say the Lean re-checked cleanly this run — for that, check lean.yml.

Running everything locally

# The Lean side
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
export PATH="$HOME/.elan/bin:$PATH"
cd lean
lake exe cache get      # pulls prebuilt Mathlib .olean, ~4 GB
lake build              # every file under MrCLean/, ~30s once cached
lake env lean MrCLean/Design.lean   # check one file in isolation

# The site side, from the repository root
npm install
npm run build           # must pass; content/snippet errors name the chapter
npm run check            # astro check, 0 errors
npm test                 # playground URLs, snippet extraction, import closures
npm run snippets:check   # every snippet, compiled as its own playground unit (needs elan)

make ci runs npm test, npm run check, and npm run build in sequence — exactly what deploy.yml runs. make snippets lists every declared region without compiling anything, useful for spotting a stale or duplicated name.

Filing a correction

Every claim on this site traces to a specific file and, usually, a specific -- SNIPPET: region or theorem name in lean/. If something looks wrong — a mistranslated statement, a hypothesis that shouldn’t be there, a stale playground link — open an issue or pull request against the repository (linked in the site footer). Name the chapter, the theorem or region, and where possible the exact discrepancy: a #print axioms result that isn’t the expected three names, a counterexample to a stated theorem, or a diff between what the prose claims and what the Lean actually says. A correction that includes a failing lake env lean invocation or a snippets:check failure is the fastest kind to act on, because it is already most of a fix.