dimension, metric signature, parity, and the result parity of multiplication
SF LEAN · JULY 21, 2026 · ALOK SINGH
An ordinary programming language
with a reason not to become Python.
A 15-minute, source-open talk: start with a record, a function, an array, and an explicit error. Then watch Lean compute 600 mixed-grade Clifford values and hand them to an interactive local view.
Slides: arrow keys · speaker notes: S · overview: Esc
A multivector field
Toggle scalar, vector, plane, and volume grades. Play 24 Lean-computed frames, orbit, zoom, and inspect exact coefficients.
Launch demo → 02 · UNDERSTAND ITPresenter tutorial
The argument, architecture, live choreography, likely questions, and permanent source-line citations.
Read tutorial → 03 · ON STAGEOne-screen cue card
The exact 12-minute route, one safe edit, recovery rules, and the closing line.
Open cue card →THE CLAIM BOUNDARY
One pipeline. Three kinds of confidence.
typed Lean program→validated scene props→JSON wire payload→local React / SVG view
Float field evaluation, explicit validation, regression tests, and 24 × 25 samples
glyph construction, camera projection, depth sorting, animation, and interaction in local JavaScript
THE STATIC PARACHUTE
The visual survives a dead editor.
This SVG is generated by Lean from the same default scene and checked byte-for-byte in preflight. It is intentionally static; the browser demo and InfoView add interaction.
Open full fallback SVG →
The narrow claim is more interesting than “Lean beats Haskell at everything.”