Vespers

Mathematical Playgrounds

Interactive explorations of tensors, hyperbolic geometry, attention mechanisms, geometric algebra, formal proofs, and historical linguistics.

Tensor Playground

Visual construction of Einstein summation expressions. Drag-and-drop tensors, connect indices, see contractions unfold in real-time.

einsum contraction tensor networks

Hyperbolic Embeddings

Dual Poincaré disk and Lorentz hyperboloid views. Draw geodesics, measure hyperbolic distances, embed hierarchical trees.

Poincaré Lorentz geodesics

Attention Visualizer

Explore self-attention mechanisms. See how queries attend to keys, visualize multi-head attention patterns, adjust temperature.

transformers QKV softmax

Geometric Algebra

Conformal Geometric Algebra sandbox. Create points, lines, circles. Apply versors, compute meets and joins, see algebraic representations.

CGA versors Clifford

Proof Tree Composer

Tactic-style proof assistant. Apply intro, induction, rewrite. Watch the proof tree grow. Export to Lean 4 or Coq syntax.

tactics type theory Curry-Howard

Historical Linguistics

Explore Semitic language families. Trace cognates across Hebrew, Arabic, Aramaic, Akkadian. Visualize sound changes and script evolution.

Semitic cognates diachronic

Category-Theoretic Computation

Witness refl loops shimmering over type nodes. Hover to expand derivations showing transport, elimination, and chained computation steps.

HoTT J-eliminator transport