Projects
Some things I’ve been building. For demos and screenshots, see Math, made tangible.
This is a second view of the same projects: a map of how they connect, by idea as well as by code. Solid arrows are direct links (one project builds on, uses or presents another). Dashed lines are conceptual links between projects that share an idea. Gray circles are private or unfinished work, left unnamed. The projects page is unchanged.
Applications
- can the land know peace — Cratons and recorded human conflict.
- Grassmann playground — based on Michael Reed’s Grassmann.jlLinked in idea to Grassmann.jl fork / Lean port
- Plain: English, made exact
- One small idea
- Hévéa Vision Pro — Unofficial Apple Vision Pro observatory for the Hévéa project’s reduced sphere (paper by Bartzos, Borrelli, Denis, Lazarus, Rohmer and Thibert). — based on the Hévéa project
- TetraGray — Lean 4 port of Michael Clark’s Tetra Gray: a general-relativistic raytracer using geometric algebra for black-hole visualization. — based on Michael Clark’s tetra-gray
- TetraGrayer — General-relativistic ray tracer in Lean 4 with Metal GPU acceleration, ported from Michael Clark’s tetra-gray. — based on Michael Clark’s tetra-gray
Mathematical research
- Jordan curve: deep points
- Lean Abstractification
- Lean Research NotebookBuilds on verso (fork)Linked in idea to Grassmann.jl fork / Lean port
- Hardy zeta: proof blueprint
- CORDIS Lean
- Verified DesignLinked in idea to Grassmann.jl fork / Lean port
- Grassmann.jl fork / Lean port — Fork of Michael Reed’s Grassmann.jl (geometric algebra), carrying the Lean port work. — based on Michael Reed’s Grassmann.jlLinked in idea to Grassmann playground, Verified Design, Hegel for Lean 4, Lean Research Notebook, Lean MCP Reliability
- Hyperreals (Julia) — Hyperreal number system implementation and formalization in Julia.
- JordanCurveTheorem — Lean 4 formalization of Kanovei–Reeken's nonstandard proof of the Jordan curve theorem, including foundations (in progress).Used by Jordan curve: deep points
- SpectralShadow — Sharp Loeb spectral visibility barrier for cut-small Lp kernels, with an exact p=2 obstruction.
Tools
- Hegel for Lean 4 — based on HegelLinked in idea to Grassmann.jl fork / Lean port
- FloatSpec — based on Hantao Lou’s FloatSpecUsed by Flocq Atlas, Flocq TraceLinked in idea to VersoCoq
- Flocq Atlas
- Flocq Trace
- Lean MCP Reliability — based on Oliver Dressler’s lean-lsp-mcpLinked in idea to Grassmann.jl fork / Lean port
- Talos: the tag-index boundary — based on Cajal Technologies’ Talos
- My SciLean fork and Metal work — based on Tomáš Skřivan’s SciLean.
- More on GitHub
- AsciiPlot — ASCII/Unicode plotting library for Lean 4 with legends and braille rendering.
- beads-lean4 — Git-backed issue tracker in Lean 4 with an agent-friendly CLI.
- Dot4 — Graphviz DOT DSL for Lean 4.
- Graph4 — Pure graph data structures and algorithms for Lean 4.
- HegelLean (Mar 2026) — Earlier, separate repo: reactive state management (signals, computed values, effects) for Lean 4.
- infnum — Python library for infinite and infinitesimal numbers using Levi-Civita fields, with PyTorch integration.Used by Derivative at a discontinuityLinked in idea to lean-inf
- iris-lean (fork) — Fork of leanprover-community’s iris-lean, the Lean 4 port of Iris (higher-order concurrent separation logic). — based on leanprover-community/iris-lean
- lean-autograd — Automatic differentiation in Lean, with Govind Pimpale, following JAX’s Autodidax tutorial.Used by LeanDidax2
- lean-inf — Levi-Civita field in Lean 4 for computing with infinities and infinitesimals.Used by Derivative at a discontinuityLinked in idea to infnum
- lean-lsp-mcp (fork) — Fork of Oliver Dressler’s Lean theorem prover MCP server. — based on Oliver Dressler’s lean-lsp-mcp
- LeanDidax2 — Pedagogical autodiff library in Lean 4 with forward/reverse modes and vectorization, inspired by JAX’s Autodidax tutorial.Builds on lean-autograd
- LeanHypothesis — Type-safe property-based testing for Lean 4 powered by Python’s Hypothesis. — based on Hypothesis
- LeanPlot — Interactive React-powered charting library for Lean 4 in the VS Code infoview.
- LeviCivita — Levi-Civita numbers for Lean 4: infinitesimals and automatic differentiation.
- Limestone — Terminal data-visualization library for Lean 4; port of Michael Chavinda’s Granite (Haskell). — based on Michael Chavinda’s Granite
- notational-fzf-vim — Notational Velocity for Vim (1.1k stars).Used by Post: My First Vim Plugin
- Projects map (this page) — This page: the project list plus a map of how the projects connect.Builds on alok.blog
- python-conceal — Vim plugin for concise Python display using Unicode subscripts and math notation.
- scilean-extra — Extensions to Tomáš Skřivan’s SciLean: Egyptian fractions, Lisp compiler, units of measurement. — based on Tomáš Skřivan’s SciLean
- tinygrad (fork) — Fork of tiny corp’s tinygrad. — based on tinygrad/tinygrad
- torch-lct-python — Differentiable linear canonical transforms and spectral layers for PyTorch (uv-installable).
- verso (fork) — Fork of Verso, the Lean documentation authoring tool (leanprover/verso). — based on leanprover/versoUsed by VersoCoq, Lean Research Notebook
- VersoCoq — Verso documentation roles for Coq/Flocq references in literate Lean 4.Builds on verso (fork)Linked in idea to FloatSpec
Selected writing and talks
- Derivative at a discontinuityBuilds on lean-inf, infnumLinked in idea to Talk: Infinitely large numbers that act like they're finite
- Broken dualities
- Closed curves are polygons, really: elementary proof of the Jordan curve theorem
- Geometric algebra as a unifying abstraction of objects and motions
- Papers and more talks
- More writing
- alok.blog — Personal blog (Jekyll on GitHub Pages).Used by Projects map (this page)
- Paper: RL environment for mathematical reasoning via program synthesis — arXiv 2107.07373.
- Post: A Field Guide to Nonstandard Definitions — Standard vs nonstandard definitions side by side (limits, continuity, derivatives).
- Post: A perfectable programming language — Interactive Lean 4 blog post arguing Lean is "perfectable".
- Post: Mechanistic Interpretability and Lean 4 — Proposal to implement ARENA in Lean.Linked in idea to ARENA_3.0 (fork)
- Post: My First Vim Plugin — 2017 post about writing notational-fzf-vim.
- Talk: Infinitely large numbers that act like they're finite — Talk on differentiating discontinuous functions with infinitesimals.Linked in idea to Derivative at a discontinuity
Other
- ARENA_3.0 (fork) — Fork of ARENA-education’s ARENA ML curriculum (interpretability, RL, evals). — based on ARENA-education/ARENA_materialsLinked in idea to Post: Mechanistic Interpretability and Lean 4
- deep-rl-course — Berkeley CS 294 Deep RL coursework.
- neetcode-gpt — GPT built from scratch, assembled from NeetCode ML course submissions.Builds on neetcode-submissions
- neetcode-submissions — NeetCode.io problem submissions.Used by neetcode-gpt
- rl_implementations — Reinforcement-learning algorithm implementations and ML experimentation.
- xai-hackathon — Personality analysis tool using Objective Personality theory with Grok.