Artificial Math
Math rewards going deep in one direction. LLMs make the sideways move cheap, which is the part I think matters. Also, who pays for the compute.
Blog
Monads, from motivic spectra to functional programming
Two pictures of monads (one from adjunctions in algebraic geometry, one from typeclasses in functional programming) are the same picture. The bridge is Kleisli.
Imandra CodeLogician: A Deep Dive into Neuro-Symbolic Code Verification
Notes on the Imandra CodeLogician paper — how neuro-symbolic methods tackle code verification with LLMs and formal reasoning working together.
The Illusion of Deep Learning
Rough notes on what some call the best ML paper of 2025. Spoiler: it's all gradient descent, apparently.
From ItaLean to Vericoding: Why I'm Now a Lean4 Fanatic
How a conference in Bologna turned me into a Lean4 evangelist and set me on the path toward vericoding.