Blog

I spent two weekends building infra, an infrastructure-as-code tool in Lean 4. It does what Terraform does: you declare the resources you want, it reads what your cloud accounts actually contain, and it reconciles the difference. Three clouds, fourteen resource kinds, about 19,000 lines of Lean, 143 commits.

It was an experiment with one question behind it. How many of the mistakes you normally discover halfway through an apply can be moved into the compiler, if the compiler has dependent types? And does that actually make the loop faster, or does it just move the pain earlier?

I work on security detection at Datadog. The model I have been building, Mambark, reads audit logs the way a language model reads text and scores every event by how surprising it is. It is a small model by today's standards, about 97 million parameters, and it looks at hundreds of billions of security events instead of sentences.

A reading note on A Theory of Deep Learning by Elon Litman (May 2026, preprint forthcoming).

The post is dense and the central derivations are sketched rather than written out. I want to fill the gaps for myself, so this note rebuilds the framework step by step and works out the algebra explicitly. The picture that emerges is a single mechanism behind four very different phenomena.

A reading note on Neural Tangent Kernel: Convergence and Generalization in Neural Networks by Arthur Jacot, Franck Gabriel, and Clément Hongler (NeurIPS 2018).

A reading note on A Primer on the Signature Method in Machine Learning by Ilya Chevyrev and Andrey Kormilitzin.

A reading note on Mamba-3: Improved Sequence Modeling using State Space Principles by Aakash Lahoti, Kevin Y. Li, Berlin Chen, Caitlin Wang, Aviv Bick, J. Zico Kolter, Tri Dao, and Albert Gu (ICLR 2026).

The best runtime check is the one that never runs.

A reading note on Sequential-Parallel Duality in Prefix Scannable Models by Morris Yau, Sharut Gupta, Valerie Engelmayer, Kazuki Irie, Stefanie Jegelka, and Jacob Andreas (ICLR 2026).