Research notes
Blogs
Short essays on AI for mathematics, scientific machine learning, formal reasoning, and the infrastructure we need for better research workflows.
01 Lean × ML
TorchLean: Verified Neural Networks in Lean
A note on why neural networks need precise meanings: shapes, graph semantics, gradients, certificates, CUDA boundaries, and scientific claims that Lean can check.
Project site: TorchLean
02 AI × Math
The Dead Ends Are the Map
Why mathematical and scientific AI systems should remember failed approaches, obstacles, partial results, and source trails, not only finished theorems.
Built with Codex over five straight days of collaborative iteration, including multiple agents for code, citations, interface cleanup, and deployment.
Companion project: Failure Atlas