MV sig pdimension, metric signature, and parity travel with each value
SF LEAN · JULY 21, 2026 · ALOK SINGH
Records, functions, arrays, errors.
One interactive multivector field.
Lean evaluates a 5 × 5 field for 24 frames. Its types carry dimension, metric signature, and parity through the program. One packed-index lemma gives kernel code a reusable bound.
On a phone: Open Slides. Swipe left to advance. Open Demo. Drag an empty part of the field to orbit. Tap a sample to inspect it. Use the grade buttons and timeline controls.
A multivector field
Use the grade buttons to show or hide scalar, vector, plane, and volume values. Play any of 24 Lean-computed frames. Drag an empty part of the field to orbit. Tap a sample to inspect its 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 12-minute route, one safe edit, recovery rules, and four factual anchors.
Open cue card →LESS BOOKKEEPING
Types that carry the algebra
Vec3→MV R3 .full→Array Sample3→InfoView
the result type computes its parity from the input types
#check, #eval, InfoView, metaprograms, and AI work against the typed program
STATIC FALLBACK
Use the SVG if the editor is unavailable.
Lean generates this SVG from the default scene. A preflight test compares it byte-for-byte with the expected SVG. The SVG is static. The browser demo and InfoView support interaction.
Open full fallback SVG →
For a conventional application, Python can be the right answer. For type-driven mathematical software, Lean lets the types go farther.