About

Why this exists

Introductions to proof assistants tend to be written for people who want a proof assistant. This one is written for a statistician or an ML researcher who wants something else: a way to know that an argument about an estimator is actually airtight, including the boring parts — the index sets, the edge case at n = 0, the place where an expectation quietly changed measure.

Design-based causal inference turns out to be an unusually good vehicle. It is finite, combinatorial and free of measure-theoretic overhead: the randomization is a uniform draw from a finite set of assignment vectors, so the probability is counting. That means the Lean can be about the substance from the first chapter rather than about plumbing.

How the Lean is verified

No Lean in these chapters is typed into the prose. Chapters name a region of a real file under lean/ — the markers are ordinary line comments — and the site lifts the text out at build time:

-- SNIPPET: ate-unbiased
theorem ate_unbiased … := by
  -- SOLUTION
  simpa using h
  -- END SOLUTION
-- END SNIPPET

A GitHub Actions job builds that directory against Mathlib on every push. Two consequences follow, and they are the reason for the whole arrangement:

• A theorem that stops compiling breaks the build, not the page. The site cannot ship a proof that no longer works.
• A chapter that refers to a region that has been renamed or deleted also breaks the build: getSnippet throws rather than emitting an empty block.

Anything genuinely unproved is written sorry, appears as sorry on the page, and is flagged as such in the surrounding prose.

How the playground works

This is a static site: there is no server here that can run Lean. Instead, every runnable block hands its code to https://live.lean-lang.org, the community lean4web instance, with the MathlibDemo project selected so import Mathlib resolves. The code travels in the URL fragment, LZ-string compressed, exactly the way lean4web itself writes it.

Clicking Run in playground expands an iframe below the block. Nothing is requested until that click, and closing the frame removes it again — which is what actually stops the language server. The New tab link is the same URL, and is what a reader with JavaScript disabled gets. Try it:

theorem two_plus_two : (2 : ℕ) + 2 = 4 := by
  norm_num

Because the playground host is a single constant (src/lib/lean.ts), pointing the whole site at a self-hosted lean4web — with this tutorial's own Lean project rather than the Mathlib demo — is a one-line change.

Colophon

Written by Drew Dimmery. The site is Astro, built to static files and served from Cloudflare Pages; the source is on GitHub.

Type is Domitian for running text, URW Classico for headings and Monaspace Argon for code, all self-hosted and subset from this site's own content at build time. Mathematics is rendered to inline SVG at build time by MathJax v4 in Neo-Euler, so math pages ship no JavaScript for it. The design, and most of the CSS, is borrowed wholesale from ddimmery.com.

The only client-side JavaScript on the site is the theme toggle, the scroll-spy that highlights the outline, and the few hundred bytes that swap the playground iframe in on click.