Projects
Some things I’ve been building. For demos and screenshots, see Math, made tangible.
Applications
- can the land know peace — Cratons and recorded human conflict.
- Grassmann playground
- Plain: English, made exact
- One small idea
Mathematical research
- Jordan curve: deep points
- Lean Abstractification
- Lean Research Notebook
- Hardy zeta: proof blueprint
- CORDIS Lean
- Verified Design
Tools
- Hegel for Lean 4
- FloatSpec
- Flocq Atlas
- Flocq Trace
- Lean MCP Reliability
- Talos: the tag-index boundary
- My SciLean fork and Metal work — based on Tomáš Skřivan’s SciLean.
- More on GitHub