Math in Sight

The mathematical idea

A ball in R^4 can be squeezed through a hole narrower than itself if we only demand that volume be preserved: shrink the first plane, stretch the second. Gromov's 1985 non-squeezing theorem says that a symplectic map cannot do this. If the ball B^4(r) embeds symplectically in the cylinder B^2(R) x R^2, then r <= R. The point is that symplectic maps, which are the maps of Hamiltonian mechanics, preserve more than volume: they remember area in the (x, y) planes.

The film uses the four coordinates as phase space for a system with two degrees of freedom, so the idea reaches mechanics. Preserving the symplectic form forces y1 to stretch when x1 is squeezed; a nonlinear Hamiltonian flow may twist and fold the ball, but the shadow on the (x1, y1) plane never drops below pi r^2. The last scene turns the cylinder so that its base is the Lagrangian (x1, x2) plane, two positions and no momentum, and then the ball fits.

How the visual was built

The scenes are WebGL (Three.js) animations of a 4-ball sampled as a point cloud, with the fourth coordinate shown by colour. The shadow on the (x1, y1) plane is measured from the points every frame and plotted live, so the viewer can watch the number stay above the floor.

The film is made by a deterministic pipeline in the project's video directory. A script file holds each line of narration with its on-screen text and a spoken respelling. A local text-to-speech model (VoxCPM2) generates one clip per line, keyed by a hash of the text, and a local Whisper model re-reads every clip to check the words. An assembly step builds the timing file and the subtitles. The picture is a page with a function renderAt(t), so any frame can be reproduced exactly. A capture script drives system Chrome through puppeteer-core, pipes PNG frames to x264, and muxes the audio.

One encoding lesson is worth recording. The file size was determined by the source, not the ffmpeg flags: sparse one-pixel point clouds plateau around VMAF 91 even at 37 Mbps. Rendering at 2x supersampling with 320,000 fainter points reached VMAF 94 at 6 Mbps, and avoiding a JPEG intermediate mattered.

What is verified and what is not

Nothing here is formally verified. The theorem is cited, not proved. What is checked is the measurement: the shadow area is computed from the actual points in each frame. The 4D-to-3D projection and the particular flows are choices made for the picture, and the labels on screen say which scene is which.

Working with AI

Claude Code wrote the WebGL scenes, the narration script and the whole video pipeline in one day (25 September 2026), with Ben steering. Ben's reactions shaped the result: he liked the Hamiltonian-flow and Lagrangian-cylinder scenes best, and asked for videos under five minutes, which at this narrator's roughly 115 words per minute meant a budget of about 550 words. The first encodes were far too large, which led to the supersampling change above.

Credits

Made by Ben Knill with Claude Code (Claude Opus). Narration: synthetic voice (VoxCPM2). Three.js from cdnjs. Page and source: github.com/BenKnill/symplectic-camel.

Proved, checked, illustrative

No formal verification. The shadow area is computed numerically each frame and plotted. The theorem is cited (Gromov, 1985), and the particular flows and the 4D-to-3D projection are chosen for the picture.

Chapters

• 0:00 A ball and a narrower cylinder
• 0:30 Four dimensions are phase space
• 1:06 How to read the picture
• 1:40 A map that is not symplectic
• 2:04 A linear symplectic squeeze
• 2:28 A nonlinear Hamiltonian flow
• 3:04 Gromov's theorem
• 3:36 A Lagrangian cylinder
• 4:07 What a symplectic map remembers
• 4:42 Outro

The mathematical idea

The kicked rotor, Chirikov's standard map, is a model of chaos: nearby orbits separate exponentially. It is also symplectic, so in principle it can be run backwards exactly. In floating point it cannot. Each step amplifies the rounding error, so a few dozen steps in, the computed inverse no longer returns the picture; only the islands of stability, where orbits are not chaotic, come home.

The fix is to move the world onto a 256 x 256 lattice. Writing the map as two shears, and rounding the kick to a whole number of cells, makes each step a permutation of cells. A permutation has an exact inverse, so every pixel returns, however chaotic the forward map is.

How the visual was built

The film uses the same deterministic pipeline as episode 1: a script file, a local text-to-speech model, ASR re-reading of every clip, a film page with a function renderAt(t), and headless Chrome capture to x264. The picture that is scrambled is the camel from episode 1. The file is 4:08 at 1080p and only about 70 MB, because the blocky three-by-three cells compress very well.

A companion lab page (Do, Undo, Repeat) puts four cards on one shared ten-cycle clock: chaos, a 30 degree rotation done by bilinear resampling versus three exact shears, the Vancouver Stock Exchange index of 1982, and the Patriot missile clock of 1991. The Patriot card reproduces the published GAO figure by chopping 1/10 to 23 fractional bits.

What is verified and what is not

The forward and backward steps exist as real AArch64 machine code, 92 bytes in all. Their correctness and the round-trip theorem are proved in HOL Light for any kick table and any n below 2^63, using the s2n-bignum ARM model, and the Hearth replay completed with no new axioms. A NEON version of the forward step, about 2.9 times faster, is proved against the same statement, which was checked term for term.

Everything outside that is checked or illustrative. The JavaScript port that draws the page matches the verified kernel at all 201 film states. The floating-point lane is ordinary double arithmetic, shown as the foil. The loop that calls the kernel, the float comparison and the drawing are not covered by the proof.

Working with AI

Claude Code wrote the pipeline, the page and, with Ben, the proofs. Proving machine code was the hard part and the failures were instructive. The simulator in the s2n-arm model decodes LD2 and ST2 only in post-indexed form, so the first NEON kernel failed to decode and was rewritten with LDP, UZP, TBL and ZIP. An array fact stated over all indices was lost at the stores until it was split into a prefix and a strict suffix. Bit-blasting 64-bit adds hung one tactic, and a single global rewrite on every assumption broke the non-overlap facts. Each lesson was written down in the repository's NOTES file so later proofs could avoid them.

Credits

Made by Ben Knill with Claude Code (Claude Opus). Narration: synthetic voice. Proofs: HOL Light with the s2n-bignum ARM model, checked through Hearth. The Vancouver and Patriot figures follow the cited public records (GAO). Page and source: github.com/BenKnill/lattice-echo.

Proved, checked, illustrative

Proved in HOL Light (via Hearth, with no new axioms): the 92-byte AArch64 forward and backward lattice steps and their round trip, for any kick table and any n < 2^63. A NEON forward kernel, about 2.9 times faster, is proved against the same statement. Checked but not proved: the page's JavaScript port matches the verified kernel at all 201 film states. Not proved: the floating-point lane is ordinary double arithmetic, shown as the foil, and the calling loop, the comparison and the drawing are outside the proof.

Chapters

• 0:00 A picture about to be scrambled
• 0:38 The kicked rotor
• 1:26 Floating point forgets
• 2:02 A grid of 256 by 256 cells
• 2:49 The machine code and its proof
• 3:41 Last time: symplectic maps
• 4:01 Outro

The mathematical idea

Episode 2 ran a chaotic map backwards exactly by moving to integers. This film asks the opposite question: how far can you trust the floating-point version? The map is a bent cat map, f(x) = x + K G(x) with K = 1/4 and the cubic G(x) = x(1 - x)(1 - 2x), on the torus. It is hyperbolic everywhere. A worst-case error analysis gives an envelope that grows geometrically with the number of steps N; the film draws that envelope as a halo.

The envelope guarantees a round trip for N up to 25 on a 256 x 256 picture. The actual builds do better than the worst case, but not by much: the plain build and the fused-multiply-add build both lose their first pixel at N = 31, six steps past the horizon. A double-double reference, which is not binary64, holds out to N = 70.

How the visual was built

The film is pixel art, not a ray-traced render. A Python program with numpy and Pillow draws every frame from recorded states and pipes them to ffmpeg, which takes about two minutes on the bluestar machine. The middle and right panels are the proved object file itself (labelled plain build, and plain build plus proof); the left panel is a second, unproven build using fused multiply-add. Every state of all eleven round trips was hashed on an Apple M5 and again under qemu, and all 535 hashes agree, so the film uses the qemu states.

The halo is the theorem's own envelope function, evaluated at K = 1/4 and drawn in pixels. When it is below a pixel, a 7 x 7 window magnified 30 times shows it at true scale; beyond that it is a blur of the same radius with a blue tint over the right panel.

What is verified and what is not

Proved in HOL Light through Hearth, with the s2n-arm-fp64 profile and no new axioms: the forward and backward step kernels are correct as machine code (12 of 12 bindings, 125 of 125 specification pins matched), and the run loop that calls them is too (18 of 18 bindings, 136 of 136 pins). The horizon is evaluated inside HOL, one matrix application at a time, so "guaranteed for N up to 25" is a theorem and not the output of a script.

Two design choices made the proof possible. Every value stays in [0, 1] by the nearest-rounding property of round-to-nearest-even, not by exactness arguments. And the mod-1 reductions compile to compare-and-branch, so the proof splits on the comparison, giving twelve paths per loop body. The cat-map kick, rather than the cubic standard map, was chosen because the standard map has islands of stability and the worst-case envelope then promises only a quarter of what floats actually deliver.

Not proved: the drawing code, and the pixel-scale presentation of the halo.

Working with AI

This was a lane run by Claude Opus under Ben's direction, with long jobs executed on the bluestar machine. Three goals were checked one at a time with pass or fail verdict lines: the native experiment, the proof, and the film. The first map choice, the standard map, failed the useful-gap test in scratch runs (horizon 27 against a first lost pixel at 123 for K = 1), which is why the map was changed.

The narration is 152 words in 13 lines from a synthetic voice, checked by speech recognition with zero word errors.

Credits

Made by Ben Knill with Claude Code (Claude Opus). Proofs in HOL Light via Hearth. Narration: synthetic voice.

Proved, checked, illustrative

Proved in HOL Light (Hearth, s2n-arm-fp64 profile, 0 new axioms): the AArch64 forward and backward step kernels (12 of 12 bindings), the run loop (18 of 18 bindings), and the envelope; the horizon N <= 25 is evaluated inside HOL, so it is a theorem. Checked, not proved: all 535 film states hash identically on the M5 and under qemu. Illustrative: the film is a 2D compositor drawing the recorded states, and the halo's pixel scale and blur are drawing choices.

The mathematical idea

In a flat, incompressible flow the vorticity is carried by the fluid, and a small concentrated patch of it behaves like a point vortex. Helmholtz's rule says vortex lines are carried with the fluid and cannot end in it, which is why a dimple at the surface must be the top of a tube that goes somewhere. For N point vortices the equations of motion are Kirchhoff's: each vortex's x and y coordinates are a conjugate pair, with the strength as a weight, and the energy is the Hamiltonian. The river surface is therefore its own phase space, in the same sense as the camel of episode 1.

The film tells the story of how the tubes arise and persist: vortices shed from the bed or from piers, smoke rings and their reconnection, and the viscous fade, a^2 plus 4 nu t. The flat picture is labelled as a model. The last act adds back the three-dimensional effects, following recent work on what dimples and scars reveal about the flow below.

How the visual was built

Two programs make the pictures. The model (vortex.js) integrates point vortices with a Scully core by the symplectic implicit midpoint rule, and advects dye particles whose enclosed area is measured. The renderer (water.js) computes the surface dip from the vortex strengths and traces rays through its Hessian: the bed brightness is 1/|det(I + k Hess eta)|, which gives a dark core with a bright caustic ring. A sun-angle offset is needed, because with an overhead sun the view ray passes through the same lens and the shadow disappears.

The film itself is a page of about 30 scenes cued to the narration, captured frame by frame with headless Chrome. The music is synthesized from scratch and ducked under the voice with sidechain compression. This draft starts and ends on Ben's own boat footage: frames from two video clips, with the dimples tracked and replayed at four times speed, grounded with swisstopo imagery and river-gauge data.

What is verified and what is not

There are no formal proofs in this episode. The simulation is checked numerically against theory: the pair speed 1.576 cm/s agrees with the formula, energy and impulses are conserved to 4e-9 and 1e-14 over 40 seconds, and the camel-shaped dye patch keeps its area to within 0.08 percent while being stretched.

The flat flow is a model, not a property of the real surface. The water renderer is an illustration. Whether the large dimples on the Rhine were shed by bed prominences is a hypothesis, supported by a published case of dimples shed from a bridge pillar on the Nidelva; there is no published dimple baseline for any river.

Working with AI

Claude Code built the models, the renderer, the page and the film. The script went through seven drafts, driven by Ben's comments and three external model reviews that caught physics errors: the flat flow is a model, Kelvin gives net zero spin, and the friend's dimples were not from oars. Ben chose a longer single story over a five-minute cut. Codex was used for assets and independently found one of the dimples in the footage. One small gotcha: the CSS uppercase rule turned a micro sign into a capital mu that read as M, so units are spelled out.

Credits

Made by Ben Knill with Claude Code (Claude Opus) and OpenAI Codex. Boat footage: our own, 1 June 2026. Aerial imagery © swisstopo. Nidelva photograph by Klervie le Bris (Aarnes et al., JFM 2025, CC BY 4.0). Music is original and synthesized; narration is a synthetic voice.

Proved, checked, illustrative

No formal proofs. Checked numerically in the project's proto/check.mjs: the pair speed 1.576 cm/s equals theory; energy and impulses are conserved to 4e-9 and 1e-14 over 40 s; the camel-shaped dye keeps its area within 0.08 percent. Illustrative: the flat 2D flow is a labelled model, and the water renderer's sky, bank and light model are an illustration. The boat footage is real.

Chapters

• 0:00 Dimples on the Rhine
• 0:43 Under the dimple
• 2:01 Smoke rings
• 3:34 The river's own smoke rings
• 4:47 What keeps one going
• 5:56 Reading the river

The mathematical idea

A soap film minimizes area, which makes it an analogue computer for geometry, but it only finds local minima. Between two plates, pins give the Steiner problem of the shortest network joining them, with the 120-degree junctions that Plateau's laws and Taylor's 1976 theorem predict. A film can settle into a network that is a local minimum but not the shortest. For six pins on a hexagon the candidate lengths are 5, the square root of 27 and the square root of 28; the shortest is five sides of the hexagon, with no junctions at all.

Between two rings, the film is a catenoid, a catenary rotated about the axis. As the rings are pulled apart the neck narrows until the catenoid ceases to exist, at the root of t tanh t = 1. Then the film snaps to two discs.

How the visual was built

The film follows a voice-first rule: the narration (517 words, 262 seconds) fixes every shot window, so each frame is rendered once at its final length. Six shots are Blender Cycles renders at 1080p, 32 samples with GPU denoising: the daylight film, a sodium-lamp version, four pins, two six-pin rigs, the catenoid and the snap, and the drain and pop. The film is a Principled BSDF with a thin-film layer of refractive index 1.33; the thickness comes from a baked flow simulation, and a studio world that is black to the camera but bright to indirect rays lets walls at every orientation show colour. Cycles' thin film is RGB, so the sodium look is a one-wavelength Airy reflectance built from shader nodes. In all, 4,192 Blender frames took about 4.9 hours of job time, roughly 2.5 hours of wall time, on one RTX 2070 shared by two jobs.

The charts, dips and proof screens are 2D renders. The Steiner shots show simulated dips run on the bluestar machine, because node versions settle some chaotic relaxations differently.

What is verified and what is not

One result is proved in HOL Light: the catenoid snap root lies in (1.1996786402, 1.1996786403) and is the unique positive root of t tanh t = 1, with no new axioms. The Steiner optima were checked by exhaustive enumeration, with gaps below 1e-7, and the minimum-area surface code reproduces the tetrahedron value 6 sqrt 2 and the cube-square value of 0.186 of the edge, which matches Surface Evolver.

The success rates in the film are simulated dips, not a tub of soap: with six pins, 506 of the first 1,000 unshaken dips found the shortest network (50.6 percent, 95 percent confidence 47.5 to 53.7). Three, four and five pins always succeed. The thin-film colours are computed physically but not validated against photographs.

Working with AI

The episode began with a friend's suggestion of minimal-surface singularities and Ben's own: the sodium-lamp stripes. The project notes record that he wanted simulations and Blender, not acrylic props. Claude Code wrote the Steiner and surface solvers, the GPU soap-flow simulation and the Blender pipeline. Claude Opus then ran the film as a lane with explicit pass or fail checks: script length, all 6,896 frames present, durations matching to 0.000 seconds, and speech recognition of every narration clip, which first failed on spellings (streetlamp, waist heard as waste) and sent five lines back for rewording. Codex worked on the Steiner success-rate lane and a live presentation version.

Credits

Made by Ben Knill with Claude Code (Claude Opus) and OpenAI Codex. Narration: synthetic voice. References: Plateau, Gergonne, J. E. Taylor (1976), and Feynman's 1983 Esalen talks and QED for the sodium-lamp idea.

Proved, checked, illustrative

Proved in HOL Light (branch codex/steiner-rate, 0 new axioms): the catenoid snap root lies in (1.1996786402, 1.1996786403) and is the unique positive root of t tanh t = 1. Checked: Steiner optima by exhaustive enumeration with gaps below 1e-7; hexagon minima 5, sqrt 27 and sqrt 28; tetrahedron 6 sqrt 2 and cube-square 0.186 of the edge (matches Surface Evolver). Simulated, not real soap: the success rates (6 pins: 50.6 percent, 95 percent CI 47.5 to 53.7). Illustrative: the thin-film colours are computed physically but not validated.

Chapters

• 0:00 A film thinner than a wavelength
• 0:32 Pins between two plates
• 1:13 Six pins, dipped twice
• 1:47 How often does it find the shortest?
• 3:00 The catenoid
• 3:25 The snap and the proved root
• 4:05 Settling down is a way to compute

The mathematical idea

The colours of a soap film encode its thickness, and in a draining, stirred film the thickness is carried by the flow like a dye. The model is the advection equation for a thickness field h in a given incompressible flow. The numerical scheme is corner transport upwind: each new cell value is a convex combination of old values, so the update obeys an exact maximum principle and the scheme cannot overshoot. A per-step error bound then composes over all 7,200 steps into a single bound, 5.9e-12, which is 413,580 times smaller than one 8-bit colour step.

How the visual was built

The simulation is the proved code itself: a 59-word AArch64 step, run in a driver, producing a 2048 by 2048 state per frame. The film shows the thickness as soap-film interference colours in Blender Cycles. Version 1 was a 60-second 1080p film at 8 samples per pixel. Version 2, shown here, was rendered at 3840 by 2160 with 256 adaptive samples, no denoiser, from the full 2048 squared state rather than a 1024 squared preview. Against a 2048-sample reference at frame 1201 the mean error is 0.026 grey levels, compared with 0.55 for version 1 with its denoiser blotches. Rendering 1,800 frames took about five hours of wall time on the bluestar machine's RTX 2070, two jobs sharing one GPU, producing 8 GB of frames. A cross-machine check compared Blender 5.2.1 on CUDA with 5.1.1 on Metal; the interior of the film agrees to a mean absolute deviation of 0.000245 in linear light.

The narrated cut follows the voice: the simulation plays at 24 frames per second after a 3-second hold, slows evenly to a stop over the last 4 seconds, and holds under the headline. It runs 86.5 seconds.

What is verified and what is not

This is the most carefully scoped claim in the series. In HOL Light, with no new axioms, three things are proved: the machine-code step, bit for bit, together with its maximum principle and error bound; the compiled driver; and the envelope over N steps. The accompanying page lists five of six claims as proved and separates the rest as checked: all 1,801 frames reproduce bit for bit from the proved object files, on the Apple M5 and, for the frames rendered on the other machine, from an x86 build of the same C source whose state hashes are equal at every step.

What is not proved is listed in plain headings on the page and repeated here. The flow is given, not derived. This is transport, not Navier-Stokes. The distance from the numerical solution to the true solution of the PDE is not bounded. The colour map is not in HOL. Nothing outside the two functions is proved, including the x86 build that wrote the frames rendered on bluestar.

Working with AI

The film was made as a lane run by Claude Opus. A frame check initially failed on a single frame because one frame in the 60-second film differs from its neighbour by less than the video's own compression error; the check was rewritten to align 15-frame stretches, and tested by confirming that a re-encode passes and that a dropped frame fails. Ben asked that long renders stay on bluestar and the Mac be used only for look-development bursts. The narration is a 14-line, 165-word script from a synthetic voice, checked by speech recognition with zero word errors.

Credits

Made by Ben Knill with Claude Code (Claude Opus) and OpenAI Codex. Renders: Blender Cycles. Proofs: HOL Light with Hearth. Narration: synthetic voice.

Proved, checked, illustrative

Proved in HOL Light (0 new axioms): the 59-word AArch64 step bit for bit, with the maximum principle and a per-step error bound; the compiled driver; and the N-step envelope (5.9e-12 over 7,200 steps). Checked, not proved: all 1,801 frames reproduce bit for bit from the proved object files. Not proved: the flow psi is given, this is transport and not Navier-Stokes, the distance to the true PDE solution, the colour map, driver I/O, the compiler, the ISA model and the render.

The mathematical idea

A Householder reflection H = I - 2 v v^T/(v^T v) is its own inverse. A program that scrambles a picture by a long sequence of reflections can undo it by applying the same reflections in reverse order, and in exact arithmetic the picture returns exactly. That makes the pair a clean test of a numerical library: failure is unambiguous.

The library in question is OpenBLAS. In the Arm64 sdot kernel that Ubuntu 26.04 ships, the result adds whatever the caller left in the vector register v0. The upstream fix ignores it. The film asks what a stray term of that kind does over a long run of reflections.

How the visual was built

The scrambled object is the series camel, a 128 by 128 RGB picture of n = 49,152 numbers. Five rounds run with N from 1,024 to 131,072 reflections each way, each step calling sdot twice. A plain C program calls cblas_sdot by name and is compiled once, then linked against the real libopenblas and against a harness shim that contains the exact kernel bytes, either shipped or patched. The harness zeroes v0 once before the first step and restores the vector registers around its per-step recorder, so v0 holds what the compiled caller leaves there and nothing is poisoned. The film is a 2D compositor drawing the recorded states; every frame matches the run on the Apple M5 bit for bit.

The finding is subtle. The main stray term, v.v at the v.x call, turns each reflection into a reflection in a moved mirror, still an involution, so most of the picture returns. The small term at the v.v call breaks the cancellation, more so the longer the run. At optimization level -O0 the stray term at the v.v call is about v.v itself and nothing returns. After the longest runs the round-trip error is between 4.4e-02 and 2.37 for the shipped kernel against 6.9e-07 to 1.2e-05 for the patched one.

What is verified and what is not

The proofs are narrow, and the film says so in its last lines. In HOL Light each 520-byte kernel is proved to compute the dot product, the shipped one plus the contents of v0 and the patched one without it. Everything else is measured. The measurements are checked against the proved model: all 2,617,344 calls equal the bit-exact function from the theorems, with zero mismatches, and the shipped kernel's bytes match the library's at the address where it lives. Runs use one thread; the threaded path for n above 10,000 is not covered by the theorems and was not measured.

Working with AI

This was a lane run by Claude Opus, with the experiment and its checks run in the dev guest on the M5. The narration for this cut was voiced by Codex: its live voice interface, driven headless through codex app-server over WebRTC, with the transcript read back as a check. Ben prefers the voices maple and vale; this cut uses maple, and a vale version exists. The earlier cut with the local text-to-speech voice is 1:28.

Credits

Made by Ben Knill with Claude Code (Claude Opus) and OpenAI Codex. Narration: Codex live voice maple. OpenBLAS is a third-party library; the shipped kernel is that of Ubuntu 26.04.

Proved, checked, illustrative

Proved in HOL Light (Hearth, s2n-arm-fp64): the narrow statements about the 520 bytes of each sdot kernel: the shipped kernel adds v0 to its answer, the fixed one ignores it. Checked: every call of 2,617,344 matches the bit-exact model of the kernel, and the library, the dlsym-resolved symbol and the extracted shipped body log identical state hashes. Measured, not proved: everything else, including the divergence curves and the behaviour at other optimization levels and thread counts.

Chapters

• 0:00 A scramble and its undo
• 0:33 The stray register v0
• 0:51 The longer the trip, the less returns
• 1:15 What the proofs cover

The mathematical idea

Floating-point addition is not associative, so a dot product computed in a different order rounds differently. The classical analysis gives a worst-case bound of the form gamma_n times the sum of |x_i y_i|. The kernel here, the Arm64 DDOT that Ubuntu ships in OpenBLAS, sums with 16 fused multiply-add lanes and a tree, and its own error bound can be proved for exactly that order. The film then asks how close real inputs can get to the bound.

Constructed inputs reach 99.6351252737 percent of the full bound at n = 4096. The film is explicit that this probes underflow and the shape of this kernel, not the optimality of the classical gamma bound.

How the visual was built

The film is a 210-second, 720p, 24 frames per second render of 5,040 frames from 2D graphics, cut to a narration of 392 words that passed a local speech-recognition check on all 33 clips. A companion page lets the viewer drag inputs and see the rounding change, and its 102 arithmetic cases are compared with an independent exact oracle.

What is verified and what is not

In HOL Light, through Hearth with the s2n-arm-fp64 profile and no new axioms, the DDOT error theorem is proved for the kernel's machine code, and a witness file evaluates the n = 1 and n = 4096 witnesses inside HOL. The 51 witnesses (best observed input at 17 lengths) also reproduce bit for bit under qemu and on the Apple M5, which ties the proved model to a real machine.

The closing section reports a different kind of result. Three identical all-ones calls to sdot returned 64, 128 and 192 on the native M5, because the shipped sdot kernel adds a leftover register. This was measured, not proved, at the time of the film; the companion film on this page, Proved vs Shipped, follows up with the proved statements. Three shipped kernels were affected in the campaign, and 53 other dot variants were not.

Working with AI

AI agents ran the lane under Ben's coordination, with Hearth, the proof-checking harness, doing the checking and a queue of long jobs on the bluestar machine and the M5. The page passed desktop dragging, reset, preset and length changes and a mobile layout check. The first narration needed edits for spoken numerals; a coordinator's 392-word speech edit is preserved next to the original text. The voice is a local text-to-speech model on the Mac.

Credits

Made by Ben Knill with Claude Code (Claude Opus). Narration: synthetic voice. The kernel analysed is OpenBLAS's Arm64 DDOT as shipped by Ubuntu.

Proved, checked, illustrative

Proved in HOL Light (0 new axioms): the DDOT error theorem, and the witness file that evaluates the n = 1 and n = 4096 witnesses. Checked: 51 witnesses reproduce bit for bit under qemu and on the Apple M5; a page test checks 102 browser arithmetic cases against an independent exact oracle. Measured, not proved: the sdot result (64, 128, 192 from identical calls).

Chapters

• 0:00 A dot product looks simple
• 0:30 Different paths, different roundings
• 1:10 The proved bound
• 1:45 Inputs that nearly reach it
• 2:25 How the proof was made
• 2:55 The sdot surprise
• 3:20 Close