Open work
Projects
Two projects that run on the same idea: in an age of cheap implementation, the scarce skill is stating precisely what must hold, and checking that it does.
A textbook
Modern Algorithm Design
Design algorithms from primitives, and know what to demand of them.
A textbook on designing algorithms from reusable primitives, and on asking precisely for what an algorithm must do.
See the project →
An open Lean library
AI Safety Formalization Atlas
The open Lean library for formal AI-safety results.
An open Lean 4 library of machine-checked AI-safety mathematics, with every result’s source and scope on record.
See the project →Where the code is
Get in touch
Press, advisory, speaking, policy work, research collaborations, or just a sharp question — the contact page reaches me directly.
ContactLast updated .