Lean's unfair advantage
SF LEAN · ALOK SINGH · JULY 21, 2026
record → function → error → array → InfoView
Follow along alok.github.io/talks/lean-unfair-advantage/
0:00-0:20. Open with the title, not the Scarf conclusion.
Say: “I want to show you Lean before the theorem prover becomes visible.”
A recent Haskell exit
7 years Haskell in Scarf production
it worked reliable code, useful types, good performance
new API work is now written in Python
why build time, libraries, and a slower development loop
The Haskell server still runs. Its share of the system is shrinking.
Avi Press, “After 7 years in production, Scarf has reluctantly moved away from Haskell,” July 10, 2026
0:20-0:50. This is only the hook. Be exact. Avi Press says Haskell delivered reliable code, caught
real bugs, and performed well. Scarf started putting new API work in a Python
server; the existing Haskell server still runs and is being reduced gradually.
The stated costs were compilation time and ecosystem friction, amplified by
parallel agent workflows.
The types did not fail. The development loop became too expensive. Move on.
If you start with types, go all the way
For a conventional application: use Python.
For type-driven mathematical software: dependent types, reusable proved facts, and programmable editor views.
The provocation: go farther than Haskell. Use Lean.
0:50-1:30.
Say: “Scarf is only a recent example. My claim is this: if I want the
conventional route, I can use Python. If I start with types for mathematical
software, I want to go farther. Lean gives me dependent types, proofs when they
save later work, and editor views built around the same values.”
Types as programming tools
ROUTINE LEAN
Write and run the program
records and functions
Array, Except, loops, IO
#check, #eval, InfoView
+
DOMAIN TYPES
Let types carry the algebra
MV R3 .full
multiplication computes result parity
the renderer receives a plain projection
Loop: edit → elaborate → evaluate → inspect.Tools: metaprograms and AI can act on the same typed program state.
Lean is officially described as both a programming language and proof assistant · lean-lang.org
1:40-2:10.
Say: “This is why I find Lean easier for this program. I can write routine
functional code, but the domain types carry facts that I would otherwise pass,
check, and keep synchronized by hand.”
Plain view data; one typed algebra
structure Vec3 where
x : Float
y : Float
z : Float
structure R3Grades where
scalar : Float
vector : Vec3
bivectorNormal : Vec3
pseudoscalar : Float
abbrev Field3 ( M : Type ) := Vec3 → M
structure Sample3 where
position : Vec3
value : R3Grades
Computed field: fieldAt : Float → Vec3 → MV R3 .fullView boundary: MV R3 p → R3Grades
Hover the ordinary view types here. In Cursor, hover fieldAt for the one dependent type used by the computation.
2:10-2:50. Open Verso's code panel and hover Vec3, R3Grades, Field3, and
Sample3. Call these plain renderer-facing types, not dependent types. In
Cursor, #check fieldAt shows Float → Vec3 → MV R3 .full.
Say: “A field is just a function from a point to a value. Here the value can
hold a number, a directed segment, an oriented plane segment, and an oriented
volume. The computation returns MV R3 .full; one adapter projects that value
to this plain record for the renderer. That is the only dependent-typing move
I need for this demo.”
Start with the program
structure PlanarGrid where
xCount : Nat
yCount : Nat
def sampleCount ( grid : PlanarGrid ) : Except String Nat := do
if grid . xCount < 2 then
throw "xCount must be at least 2"
return grid . xCount * grid . yCount
#eval Except.ok 9 sampleCount { xCount := 3 , yCount := 3 }
Except.ok 9
#eval Except.error "xCount must be at least 2" sampleCount { xCount := 1 , yCount := 3 }
Except.error "xCount must be at least 2"
This slide is a Lean file. Verso type-checked the code while building the deck.
2:50-3:15. Click sampleCount if you want Verso's code info panel, but do not
linger. This slide is also the fallback if the editor is unavailable.
Say: “A record, a function, an explicit error, and a result. Lean runs it. The
deck is also a Lean file, so Verso checked this block when it built the slides.”
Live: ordinary programming
PlanarGrid → function → Except String (Array Sample)
read the result
change 3 × 3 to 4 × 3
run invalid input and read the error
Switch to Cursor · OrdinaryProgrammingDemo.lean
3:15-9:45. Switch to Cursor.
In OrdinaryProgrammingDemo.lean, show tinyGrid, swirlField, and
sampleCount.
Put the cursor on the successful #eval: Except.ok 9.
Edit only xCount := 3 to xCount := 4; show Except.ok 12.
Show the final invalid-grid command and its explicit error.
Switch to MultivectorFieldDemo.lean, click #html, toggle grade 2 off/on,
play/pause, drag the empty background once, and reset.
If someone asks what the picture establishes, say: “Lean computed these
numbers; I am not claiming the picture is a proof.”
After the visual, return to this deck and advance once.
What Lean and the view do
Lean computes and validates the field values.The view draws them and handles the camera and controls.
9:45-10:45.
Say: “GrassmannFields does not know about the renderer. GrassmannViz adds
the scene and InfoView. Lean sends positions and coefficients; the view turns
them into marks on the screen.”
The one dependent type in this demo
MV R3 .fullthis field has the R3 metric and may contain every grade
MV R3 .eventhe rotor can contain only even grades
.even * .full = .fullmultiplication computes the result parity
R3Grades.ofMVone explicit boundary produces plain view data
browser demo · presenter tutorial · one-screen cue card
10:45-12:00.
Say: “I am not claiming that every record here is dependently typed. Vec3 and
R3Grades are deliberately plain. The useful type is MV R3 .full: the field's
dimension, metric, and allowed grades travel together. The rotor is
MV R3 .even, and multiplication determines that the result is full. Then one
explicit adapter produces plain renderer data. The point is to use just enough
type structure to make the next change easier.”
Stop at 12:00 and use the remaining three minutes for questions.
