William
Chang

How the Lean proof assistant checks a proof, one tactic at a time; what a theorem rests on; why two proofs of the same fact can be genuinely different; and a game where the shortest proof is usually a lemma someone already proved.

Fold paper by hand in a bar-and-hinge simulator, teach a folded tube to crawl with no wheels, and download a printable template, servo plan and Arduino code to build the real robot.

Build parts out of logic gates, assemble them into bigger parts, and wire one up as a robot's brain. The example robot follows a line using two inverters made from NAND gates.

Which requests should the $0.001 model get, and which the frontier model? Drop in an eval log, set a quality target, and get the cheapest cascade or router that meets it, certified on held-out prompts. Runs in your browser.

Everyone in the room scans a QR code and types one phrase; the phrases land on a big-screen map where similar ones sit together. Find yourself, find your neighbours, and see what “similar” means to a model.

A recommender only learns from what it shows, so it keeps showing what it already knows. Rate a dozen things, watch 400 readers' feeds narrow over 30 rounds, then switch on exploration and see the catalogue open back up.

A puzzle game about data leakage: eight models that score too well, and you guess what each is really using before it retrains without its shortcut. Then run the same checks on your own CSV.

Two-wheeled robots shoving each other out of a ring. Small neural nets trained by evolution strategies and self-play. Drive one yourself and try to beat each level.

A chess engine that learned its own piece values by playing itself, starting from all pieces equal. Play against any of its four levels.

Drop in a song and get a simplified piano arrangement: the chords, the melody and sheet music you can play. Beat, chord and melody detection run in your browser.

Sheet music you write together, like a shared doc. Type or tap in notes, hear them played back, and invite people to edit the same score live, with cursors and version history.

Sing six notes and a few words, pick any song, and hear its melody sung back in your own voice. Pitch shifting by PSOLA, all in the browser.

Pull the singer out of a song, right in your browser: drop in a track and get the voice and the backing as separate files. No training data, nothing uploaded.

Load a song, paste timestamped lyrics (or tap along to time them), and turn them into an animated lyric video whose scene follows the song's mood, read by a small model that runs in your browser. Exports the finished video.

Drop in a CSV and find the problems that quietly break machine-learning models: leaking columns, test rows copied from training, contradictory labels, hidden placeholders. Then download the fix.

When a multi-step LLM pipeline gets an answer wrong, find which step caused it. Swap steps for better versions with the randomness held fixed, and watch Shapley values split the blame.

Race bandit algorithms against the Lai–Robbins lower bound in your browser, and plan an A/B test: see whether a fixed split or Thompson sampling costs fewer conversions.

See how far to trust a classifier: honest confidence, prediction sets with a coverage guarantee, abstention with a certified error rate and drift alarms. Try it on three models or your own CSV.

Five ideas from ML theory you can play with in the browser: double descent, high-dimensional geometry, diffusion models that copy their training data, private polls and certified robustness.

A shared bucket list sorted like ski runs, from easy nights in to passport trips. Make an account, start a list and invite people to it.

Describe a math figure in words and get an interactive one you can rotate, slice and share. Starts with a drilled sphere, solids of revolution, Riemann sums and more.