Independent researcher, systems architect, and creative technologist
I build auditable AI systems, formal tools, and interactive media鈥攖urning ambitious ideas into inspectable, reproducible work.
Featured work 路 All repositories 路 Sponsor open work 路 Music
I build things that shouldn鈥檛 exist yet. Then I make them rigorous.
- Auditable AI and verification: tools that bind computational claims to evidence, checking mechanisms, provenance, and explicit limits.
- Formal and mathematical systems: executable research across Lean, ordinal arithmetic, logic, and the broader hyperfield ecosystem.
- Creative technology: AI-assisted games, music systems, creator tools, and experiments that make difficult ideas tangible.
| Project | What it does |
|---|---|
| Verifier | Implements the Verifier Standard (VSTD) for portable, bounded, refutable computational evidence and provenance graphs. |
| Lean4 Explainer | Builds navigable proofsites from Lean 4 code using an explanation layer designed for higher-order specificity. |
| Hyperfields | Provides a Lean 4-checked, source-pinned map of the public hyperfield ecosystem. |
| Hypermath | Develops a formal universe from one primitive operation, with a Lean translation and explicit open proof obligations. |
| Ordinatics | Explores exact ordinal arithmetic and bounded typed satisfaction in an ordinal-first computational framework. |
- Evidence before confidence.
- Reproducible artifacts before broad claims.
- Open obligations and unknowns stated plainly.
- Ambitious ideas paired with mechanisms that can be inspected, tested, and challenged.
I publish open research, tools, experiments, and documentation across AI, computation, mathematics, and creative systems. If that work helps you think, build, or verify something more effectively, sponsorship helps fund more of it.
For a project-specific question or collaboration idea, open an issue in the relevant repository with a concrete use case, counterexample, or proposal.