Teerth Sharma

teerth.blog

Teerth Sharma

Long-form essays on the projects, with the maths, the proofs and the numbers.

essays
14
words
64,000
upstream changes they led to
12
Read the essaysteerth.dev
resolvent: heat-map of (I − γP)⁻¹The resolvent M = (I − γP)⁻¹ of an 8-state Markov chain with two blocks of four states, γ = 0.9, drawn as a heat-map on a sequential scale from 0 to 2.5. Every row sums to 10 = 1/(1−γ). The cover fills the partial sums Σₖ≤K (γP)ᵏ hop by hop until they reach M.2.50M[i,j]γ = 0.9Σⱼ S = 10= 1/(1−γ)resolvent · (I − γP)⁻¹hops ∞caustic: twenty entities collapsing onto one answerTwenty entities on the left map to a single answer on the right, so they form 1 orbit of the answer map; the certified error floor is 1 − 1/20 = 0.950.entitiesanswers201floor 1 −1/20= 0.950caustic · orbit partition of the answer map20 →  1Epsilon-Hollow: nearest centroid with a certificateA query moves along a great circle on the unit sphere. Each frame the nearest centroid is searched in its grid block and certified when it lies inside the cap of radius equal to the block boundary distance; otherwise the cap is hatched and a full scan answers.CERTIFIEDd 0.367bound 0.869nearest #3Nearest centroid · S² · K = 8CERTIFIED margin +0.502nerve: two linked polymer rings with over and under crossingsTwo closed 24-bead rings projected to the plane. Ring B slides through ring A and back; in the linked still they cross 2 times, the crossing signs sum to 2, and the Gauss linking number is 1.Σ signs+1 +1Lk = 1nerve · linked rings, Gauss Lk2 crossingsmonodromy: the log-polar helicoid, two lapsThe map (x, y) ↦ (eˣ cos y, eˣ sin y) lifted to a helicoid over two full laps. A point p climbs one lap from the red point q; its image goes once round the origin and returns to f(q), so the two red points share an image (dashed fibre, grey ring) although the determinant of the Jacobian, e²ˣ, is positive everywhere: the map is a local but not a global inverse.qpf(p) = f(q)monodromy · log-polar helicoiddet Df = 1.11 > 0Electromagnetic-Field-Data-Simulator: E and B field lines with the Faraday tensorElectric field lines (indigo) leave a positive charge that drifts toward the wire, for a fixed negative charge; magnetic field lines (teal) circle a wire whose current reverses over the loop. At the probe, E and B fill the antisymmetric 4×4 Faraday tensor on the right, and the readout is the invariant I₁ = B² − E².Fᵘᵛ++−−−++−EBEM field simulator · E, B, FI₁ = −0.15

The family

Where the work went

Four lines of work as a family tree, one lane each: what each project was built on or came out of, and the upstream pull requests it led to. Every line is a link the author has confirmed.

Relations in the family: topological-ml-toolkit is built on Aether-Lang. monodromy came out of topological-ml-toolkit. nerve came out of topological-ml-toolkit. separatrix came out of Epsilon-Hollow. tangle came out of Epsilon-Hollow. planimeter came out of Epsilon-Hollow. faraday is in the same line of work as resolvent. Electromagnetic-Field-Data-Simulator came out of faraday. Asmodeus came out of resolvent. Asmodeus came out of caustic. sigmoid came out of caustic. sigmoid came out of Epsilon-Hollow. topological-ml-toolkit, monodromy, nerve form one group, topological tools, under Aether-Lang. topological tools led to triton-lang/kernels pull request 22: topology-derived sparse attention, 3.48× at 4K context. topological tools led to google/XNNPACK pull request 10801: memory planner reuses leading gaps, FP32 MobileNet V1 peak allocation 6.42% lower. topological tools led to google/highway pull request 3244: PHAST build 1.65× to 1.98× faster at 1,000,000 keys, output digests identical. topological-ml-toolkit led to google-deepmind/mujoco pull request 3396: island discovery on a disjoint-set forest, 1,281× less solver memory. topological-ml-toolkit led to NVIDIA/topograph pull request 432: chart RBAC rules gated by engine and provider. nerve led to open2c/polychrom pull request 79: getLinkingNumber sign fix. Epsilon-Hollow led to openxla/xla pull request 46539: deterministic GPU reduction grouping, landed as 3d5df1d. Epsilon-Hollow led to tensorflow/tensorflow pull request 124410: exact transitive closure of collective control edges. Epsilon-Hollow led to NVIDIA/NeMo-Relay pull request 481: cross-process agreement 0.48 → 1.00. Epsilon-Hollow led to google-deepmind/mujoco pull request 3450: convex hull graph without the quadratic scan, 4.21× faster cold load at 40,962 vertices. Epsilon-Hollow led to google-deepmind/mujoco_warp pull request 1541: island discovery on a GPU disjoint-set forest, scratch memory down 97.73%. caustic led to facebook/pyrefly pull request 4180: test capturing a capped-recheck propagation panic, landed as 3e90baa.

  1. Aether-Lang: a Vietoris–Rips complex with its Betti vectorThirteen points on a noisy ellipse and the Vietoris–Rips complex at radius 1.16 (24 edges, 11 triangles). The Betti vector is [1, 1, 0] and has stayed unchanged for 0.51 of radius. The stop rule (unchanged for 0.50) fired at r = 1.15 and holds.r = 1.16β = [1, 1, 0]held ≥ 0.50stop: β heldAether-Lang · Vietoris–Rips at one radiusβ=[1,1,0]Aether-LangEssay 08 · 22 mintopological-ml-toolkit: a point cloud and its persistence diagramLeft: 18 points (a noisy circle of 14 with four stragglers) with their Vietoris–Rips 1-skeleton at r = 0.93, past the last death, so no loop is left. Right: the complete persistence diagram of the same filtration: 17 finite H0 classes on the vertical axis, one essential H0 class at infinity, and 3 H1 classes; the longest is born at 0.65 and dies at 0.98. In motion the radius sweeps up and back, the loop's wash shows while that class is alive, and the readout counts pairs.Rips r = 0.93 · b1 3∞0110birthdeathtopological-ml-toolkit · persistence diagram18 pairstopological-ml-toolkitbuilt on Aether-LangEssay 09 · 22 minmonodromy: the log-polar helicoid, two lapsThe map (x, y) ↦ (eˣ cos y, eˣ sin y) lifted to a helicoid over two full laps. A point p climbs one lap from the red point q; its image goes once round the origin and returns to f(q), so the two red points share an image (dashed fibre, grey ring) although the determinant of the Jacobian, e²ˣ, is positive everywhere: the map is a local but not a global inverse.qpf(p) = f(q)monodromy · log-polar helicoiddet Df = 1.11 > 0monodromycame out of topological-ml-toolkitEssay 11 · 21 minnerve: two linked polymer rings with over and under crossingsTwo closed 24-bead rings projected to the plane. Ring B slides through ring A and back; in the linked still they cross 2 times, the crossing signs sum to 2, and the Gauss linking number is 1.Σ signs+1 +1Lk = 1nerve · linked rings, Gauss Lk2 crossingsnervecame out of topological-ml-toolkitEssay 10 · 20 minopen2c/polychrom #79getLinkingNumber sign fixgoogle-deepmind/mujoco #3396island discovery on a disjoint-set forest, 1,281× less solver memoryNVIDIA/topograph #432chart RBAC rules gated by engine and providertriton-lang/kernels #22topology-derived sparse attention, 3.48× at 4K contextgoogle/XNNPACK #10801memory planner reuses leading gaps, FP32 MobileNet V1 peak allocation 6.42% lowergoogle/highway #3244PHAST build 1.65× to 1.98× faster at 1,000,000 keys, output digests identical
  2. Epsilon-Hollow: nearest centroid with a certificateA query moves along a great circle on the unit sphere. Each frame the nearest centroid is searched in its grid block and certified when it lies inside the cap of radius equal to the block boundary distance; otherwise the cap is hatched and a full scan answers.CERTIFIEDd 0.367bound 0.869nearest #3Nearest centroid · S² · K = 8CERTIFIED margin +0.502Epsilon-HollowEssay 07 · 21 minopenxla/xla #46539deterministic GPU reduction groupinglanded as 3d5df1dtensorflow/tensorflow #124410exact transitive closure of collective control edgesNVIDIA/NeMo-Relay #481cross-process agreement 0.48 → 1.00google-deepmind/mujoco #3450convex hull graph without the quadratic scan, 4.21× faster cold load at 40,962 verticesgoogle-deepmind/mujoco_warp #1541island discovery on a GPU disjoint-set forest, scratch memory down 97.73%separatrix: a top-3 boundary straddled by an interval enclosureTen scores with rounding enclosures that tighten and widen again. The top 3 lie above the dashed boundary; at the still's half-width 0.14 the lower end of the weakest member (0.58) does not clear the upper end of the strongest outsider (0.70), so the hatched band marks a boundary that cannot be certified. As the enclosures narrow the corridor opens and the verdict becomes certified.k = 3separatrix · top-k with interval enclosuresREFUSEDseparatrixcame out of Epsilon-HollowEssay 05 · 23 mintangle: a crossing too flat to read, so the linking number is the interval [0, 1]Two strands cross and the over-strand turns against the under-strand. Where the angle is too flat (|sin θ| below 0.15) the crossing cannot be read and is hatched; the linking number is then the interval [0, 1]. Where the angle is clear the crossing is certified with its sign and the interval collapses to one integer.?det +0.12UNKNOWN-1012lk ∈ [0, 1]tangle · lk from one crossingREFUSEDtanglecame out of Epsilon-HollowEssay 04 · 16 minplanimeter: an axonometric floor plan with its enclosed rooms shaded and countedWalls of a 10 by 6 plan, drawn one piece at a time and extruded above the floor. The finished plan has 12 vertices, 16 edges and 1 connected component, so E − V + C = 5 bounded faces, the 5 shaded rooms, each lifted as its last wall lands.12345planimeter · rooms = E − V + CV 12 · E 16 · F 5planimetercame out of Epsilon-HollowEssay 06 · 18 min
  3. sigmoid: H0 barcode beside its minimum spanning treeFourteen points in two loose clusters, shaded by cluster, joined by their minimum spanning tree; the H0 barcode beside it has thirteen finite bars with exactly the lengths of the tree edges, and the fourteenth bar never dies. The dashed edge is the bridge between the two clusters and is the longest finite bar.εsigmoid · H₀ barcode = MST edgesβ₀ 14 → 1sigmoidcame out of caustic and Epsilon-HollowEssay 02 · 21 min
  4. caustic: twenty entities collapsing onto one answerTwenty entities on the left map to a single answer on the right, so they form 1 orbit of the answer map; the certified error floor is 1 − 1/20 = 0.950.entitiesanswers201floor 1 −1/20= 0.950caustic · orbit partition of the answer map20 →  1causticEssay 03 · 23 minfacebook/pyrefly #4180test capturing a capped-recheck propagation paniclanded as 3e90baa
  5. Asmodeus: the time traveller reading an eraA softmax decider (the time traveller) holds a weight over four eras, each an order-1 count table, on a stream whose law switches and recurs. At this instant it answers alone from era C: top weight 1.00 against the threshold 0.9. The dashed arc runs from now back to the earlier stretch where that era last held; the boxed cell in each table is the transition being scored.10P(x|x′)ABCDnowtrue eraTT weightθ = 0.9A 0.00B 0.00C 1.00D 0.00asmodeus · time traveller over 4 erasalone · v 1.00Asmodeuscame out of resolvent and causticEssay 14 · 23 min
  6. resolvent: heat-map of (I − γP)⁻¹The resolvent M = (I − γP)⁻¹ of an 8-state Markov chain with two blocks of four states, γ = 0.9, drawn as a heat-map on a sequential scale from 0 to 2.5. Every row sums to 10 = 1/(1−γ). The cover fills the partial sums Σₖ≤K (γP)ᵏ hop by hop until they reach M.2.50M[i,j]γ = 0.9Σⱼ S = 10= 1/(1−γ)resolvent · (I − γP)⁻¹hops ∞resolventEssay 01 · 16 minfaraday: a cavity eigenmode as a contour mapContour map of a degenerate eigenmode of a square cavity, sin(πx)sin(3πy) + sin(3πx)sin(πy), eigenvalue k² = 10π². Orange contours are positive, blue contours negative, and the grey lines are the nodal lines.u > 0u < 0u = 0k² =10π²u = ψ·cos 2πtfaraday · cavity eigenmode ψcos 2πt = +1.00faradaysame line of work as resolventEssay 12 · 19 minElectromagnetic-Field-Data-Simulator: E and B field lines with the Faraday tensorElectric field lines (indigo) leave a positive charge that drifts toward the wire, for a fixed negative charge; magnetic field lines (teal) circle a wire whose current reverses over the loop. At the probe, E and B fill the antisymmetric 4×4 Faraday tensor on the right, and the readout is the invariant I₁ = B² − E².Fᵘᵛ++−−−++−EBEM field simulator · E, B, FI₁ = −0.15Electromagnetic-Field-Data-Simulatorcame out of faradayEssay 13 · 18 min
  • built on
  • came out of
  • led to an upstream pull request
  • same line of work

Each project links to its essay, each upstream node to its pull request. Only links the author has confirmed are drawn.

Essays

One essay per project

One per project: the problem, why it is hard, the maths, the proofs, what was measured and what failed.

Attention & learning

3 essays
resolvent: heat-map of (I − γP)⁻¹The resolvent M = (I − γP)⁻¹ of an 8-state Markov chain with two blocks of four states, γ = 0.9, drawn as a heat-map on a sequential scale from 0 to 2.5. Every row sums to 10 = 1/(1−γ). The cover fills the partial sums Σₖ≤K (γP)ᵏ hop by hop until they reach M.2.50M[i,j]γ = 0.9Σⱼ S = 10= 1/(1−γ)resolvent · (I − γP)⁻¹hops ∞

Essay 01

resolvent

A JEPA planner ranks candidate futures one at a time. When they share one error, the right pick depends on the whole candidate set.

0.732 / 0.703 / 0.787normalised score, D-JEPA-spec operator at ε = 4, K = 63, full shared error, 3 seedsControl: D-JEPA as specified (ε = 0.2): 0.352 / 0.354 / 0.358
  • Python
  • Lean 4
3,681 words · 16 min
sigmoid: H0 barcode beside its minimum spanning treeFourteen points in two loose clusters, shaded by cluster, joined by their minimum spanning tree; the H0 barcode beside it has thirteen finite bars with exactly the lengths of the tree edges, and the fourteenth bar never dies. The dashed edge is the bridge between the two clusters and is the longest finite bar.εsigmoid · H₀ barcode = MST edgesβ₀ 14 → 1

Essay 02

sigmoid

Measuring the shape of a trained model's activations as a state, and rolling that state forward with one ridge solve instead of a second network.

0.855island partition read from ψ, probe accuracy on the S²-Rips corpusControl: PCA channel 0.469 · majority class 0.487
  • Python
4,844 words · 21 min
caustic: twenty entities collapsing onto one answerTwenty entities on the left map to a single answer on the right, so they form 1 orbit of the answer map; the certified error floor is 1 − 1/20 = 0.950.entitiesanswers201floor 1 −1/20= 0.950caustic · orbit partition of the answer map20 →  1

Essay 03

caustic

A model can hold a fact and still fail to reach it. When it fails, distinct entities collapse onto one answer, and the collapse proves errors.

0.950certified error floor on 20 country–capital prompts behind 128 tokens of " the", computed from the model's answers aloneControl: 128 tokens of coherent prose: floor 0.000; measured error 0.000, against 1.000 behind the repeated token
  • Python
5,353 words · 23 min

Certificates

3 essays
tangle: a crossing too flat to read, so the linking number is the interval [0, 1]Two strands cross and the over-strand turns against the under-strand. Where the angle is too flat (|sin θ| below 0.15) the crossing cannot be read and is hatched; the linking number is then the interval [0, 1]. Where the angle is clear the crossing is certified with its sign and the interval collapses to one integer.?det +0.12UNKNOWN-1012lk ∈ [0, 1]tangle · lk from one crossingREFUSED

Essay 04

tangle

From a photo of two cables: an integer linking-number certificate, or a refusal that names the crossing to re-shoot.

0wrong certificates over 2,000 closed-braid diagrams and 80 rendered scenes; 0 of 247 real photographs certifiedControl: abstain-on-any-unknown also 0 wrong; a coin flip on the same unknowns: 755 and 47 wrong
  • Python
3,596 words · 16 min
separatrix: a top-3 boundary straddled by an interval enclosureTen scores with rounding enclosures that tighten and widen again. The top 3 lie above the dashed boundary; at the still's half-width 0.14 the lower end of the weakest member (0.58) does not clear the upper end of the strongest outsider (0.70), so the hatched band marks a boundary that cannot be certified. As the enclosures narrow the corridor opens and the verdict becomes certified.k = 3separatrix · top-k with interval enclosuresREFUSED

Essay 05

separatrix

Tells you whether a top-k list came from your data or from the computer's rounding, and refuses, naming the pair, when it cannot tell.

0 of 1,116certified top-10 sets moved across nine numerically distinct enginesControl: all 8 sets that did move had been refused first (one draw, seed 11)
  • Python
5,240 words · 23 min
planimeter: an axonometric floor plan with its enclosed rooms shaded and countedWalls of a 10 by 6 plan, drawn one piece at a time and extruded above the floor. The finished plan has 12 vertices, 16 edges and 1 connected component, so E − V + C = 5 bounded faces, the 5 shaded rooms, each lifted as its last wall lands.12345planimeter · rooms = E − V + CV 12 · E 16 · F 5

Essay 06

planimeter

An agent edits a drawing and reports the room count. planimeter reads the file and returns the count, or the coordinate where the file cannot say.

0 wrongintegers on 528 constructed drawings: 495 exact, 33 refusedControl: same 528 files: round-6 snap 350 wrong, shapely polygonize_full 336 wrong
  • Python
4,172 words · 18 min

Systems & languages

2 essays
Epsilon-Hollow: nearest centroid with a certificateA query moves along a great circle on the unit sphere. Each frame the nearest centroid is searched in its grid block and certified when it lies inside the cap of radius equal to the block boundary distance; otherwise the cap is hatched and a full scan answers.CERTIFIEDd 0.367bound 0.869nearest #3Nearest centroid · S² · K = 8CERTIFIED margin +0.502

Essay 07

Epsilon-Hollow

A research kernel that keeps its state as points on a sphere and returns each discrete answer with a certificate that rounding could not change it, or refuses.

1,215 → 0wrong nearest-centroid answers in 5,000 seeded queries, before and after the certificateControl: reported hit rate 1.0000 before, 0.9818 after; stated on the project page, not re-measured
  • Rust
  • Lean 4
4,799 words · 21 min
Aether-Lang: a Vietoris–Rips complex with its Betti vectorThirteen points on a noisy ellipse and the Vietoris–Rips complex at radius 1.16 (24 edges, 11 triangles). The Betti vector is [1, 1, 0] and has stayed unchanged for 0.51 of radius. The stop rule (unchanged for 0.50) fired at r = 1.15 and holds.r = 1.16β = [1, 1, 0]held ≥ 0.50stop: β heldAether-Lang · Vietoris–Rips at one radiusβ=[1,1,0]

Essay 08

Aether-Lang

A research language where persistent homology is a primitive, so a loop can stop when the Betti numbers of its data stop changing.

[1, 1, 0]Betti vector at which the README tour's seal loop stops, at radius 1: one piece, one loopControl: printed by the tour program; not compared against a tuned scalar stopping rule
  • Rust
  • Lean 4
  • Aether
5,086 words · 22 min

Topology tooling

3 essays
topological-ml-toolkit: a point cloud and its persistence diagramLeft: 18 points (a noisy circle of 14 with four stragglers) with their Vietoris–Rips 1-skeleton at r = 0.93, past the last death, so no loop is left. Right: the complete persistence diagram of the same filtration: 17 finite H0 classes on the vertical axis, one essential H0 class at infinity, and 3 H1 classes; the longest is born at 0.65 and dies at 0.98. In motion the radius sweeps up and back, the loop's wash shows while that class is alive, and the readout counts pairs.Rips r = 0.93 · b1 3∞0110birthdeathtopological-ml-toolkit · persistence diagram18 pairs

Essay 09

topological-ml-toolkit

Persistent homology as ordinary ML features, with a certificate that decides when one barcode can stand in for a whole moving point cloud.

1 of 3persistence evaluations for a certified three-frame trajectory; every diagram equals dense recomputation within rtol 1e-10Control: dense per-frame recomputation: 3 of 3
  • Rust
  • Python
  • C++
  • x86-64 assembly
  • CUDA
5,032 words · 22 min
nerve: two linked polymer rings with over and under crossingsTwo closed 24-bead rings projected to the plane. Ring B slides through ring A and back; in the linked still they cross 2 times, the crossing signs sum to 2, and the Gauss linking number is 1.Σ signs+1 +1Lk = 1nerve · linked rings, Gauss Lk2 crossings

Essay 10

nerve

Can a local atomic descriptor see how polymer chains are linked and knotted? A Rust harness that counts what the descriptor merges.

3 of 4blindness hypotheses withdrawn by the repository's own controls; the fourth survives only while the strands are farther apart than the cutoffControl: each withdrawal names what killed it: a same-architecture seed-noise floor, a measured |Lk| significance of 1.2327 instead of 0.1 by eye, and the 2-body residual at the same cutoff
  • Rust
4,700 words · 20 min
monodromy: the log-polar helicoid, two lapsThe map (x, y) ↦ (eˣ cos y, eˣ sin y) lifted to a helicoid over two full laps. A point p climbs one lap from the red point q; its image goes once round the origin and returns to f(q), so the two red points share an image (dashed fibre, grey ring) although the determinant of the Jacobian, e²ˣ, is positive everywhere: the map is a local but not a global inverse.qpf(p) = f(q)monodromy · log-polar helicoiddet Df = 1.11 > 0

Essay 11

monodromy

Testing whether a map can be run backwards by comparing pairs of points, instead of checking its Jacobian one point at a time.

8/8maps classified correctly on the repo's benchmark (ρ path, Jacobian passed in)Control: determinant test on the same eight maps: 6/8
  • Python
4,832 words · 21 min

Fields

3 essays
faraday: a cavity eigenmode as a contour mapContour map of a degenerate eigenmode of a square cavity, sin(πx)sin(3πy) + sin(3πx)sin(πy), eigenvalue k² = 10π². Orange contours are positive, blue contours negative, and the grey lines are the nodal lines.u > 0u < 0u = 0k² =10π²u = ψ·cos 2πtfaraday · cavity eigenmode ψcos 2πt = +1.00

Essay 12

faraday

Counts where a cavity mode's electric nodal lines meet the wall and where its magnetic field curls inside, and tests the exact law between the two.

132 of 132TM modes of 11 cavities obey Q = χ(D) + N_wall/2, from a rectangle to a disk with two holesControl: a distractor term in the least-squares fit gets weight 0.0000; on a 15 × 15 grid the same check fails on 25 of 320 signature entries
  • Python
4,325 words · 19 min
Electromagnetic-Field-Data-Simulator: E and B field lines with the Faraday tensorElectric field lines (indigo) leave a positive charge that drifts toward the wire, for a fixed negative charge; magnetic field lines (teal) circle a wire whose current reverses over the loop. At the probe, E and B fill the antisymmetric 4×4 Faraday tensor on the right, and the readout is the invariant I₁ = B² − E².Fᵘᵛ++−−−++−EBEM field simulator · E, B, FI₁ = −0.15

Essay 13

Electromagnetic-Field-Data-Simulator

A Rust, Python and TypeScript toolkit that builds the Faraday tensor from sampled E and B fields and summarises the energy map as a graph.

3implementations of one Faraday-tensor pipeline: Rust, Python, TypeScriptControl: no test compares the three; each test file imports only its own module
  • Rust
  • Python
  • TypeScript
4,063 words · 18 min
Asmodeus: the time traveller reading an eraA softmax decider (the time traveller) holds a weight over four eras, each an order-1 count table, on a stream whose law switches and recurs. At this instant it answers alone from era C: top weight 1.00 against the threshold 0.9. The dashed arc runs from now back to the earlier stretch where that era last held; the boxed cell in each table is the transition being scored.10P(x|x′)ABCDnowtrue eraTT weightθ = 0.9A 0.00B 0.00C 1.00D 0.00asmodeus · time traveller over 4 erasalone · v 1.00

Essay 14

Asmodeus

A stream whose law changes, then comes back. Asmodeus keeps one small table per law and a softmax over them, so a returning law is recalled, not re-learned.

11×lower regret against an oracle than the best owned online learner, on streams of 4 recurring laws, 10 fresh seeds: 0.0277 vs 0.3056 nats per tokenControl: the best owned learner (BOCPD), tuned on separate seeds; when no law ever returns, the era bank costs 1.18× BOCPD (0.0186 vs 0.0159)
  • Python
  • Lean 4
5,226 words · 23 min