Things I Build

Rigorous formal logic, disguised as addictive puzzle adventures.

A deduction game of hundreds of hand-crafted original logic puzzles: truth-tellers, liars, and stranger logics, set across a world of constantly expanding islands. Live now on the App Store and Google Play. Co-created with Nadia Gasmi.

Turning messy system data into machine-checked safety guarantees.

Building an end-to-end pipeline that ingests multi-modal data from real cyber-physical systems (think drone flight logs), uses tools for surfacing anomalies and behavioral constraints, and formalizes the resulting requirements, safety constraints and certain certificates on behavior in Lean 4 using sheaf toposes via temporal type theory, producing proofs of system-level safe behavior that a machine can check. The aim is principled compliance you can actually verify, scalable across systems whose parts behave very differently. Message me if you're interested in this. Stealth startup for now. But also doing some consulting if you have Lean problems.

Manifold learning that respects how systems move through time.

Most dimensionality-reduction tools flatten time or have trouble with it. Developed XMAP to overcome these shortcomings: a type-driven, sheaf-theory-inspired extension of manifold-learning methods (the UMAP family) to time-varying data, built to keep the structure that matters, surfacing regime shifts, dispersion events, and pivots cleanly, for instance in high-dimensional financial trajectories, while staying interpretable and mathematically transparent. Private for now, but message if interested.