We are Problem Solvers
A reminder that we are problem solvers, and that the human mind is still the strangest thing we know of.
Writing
This section collects notes on formal verification, mathematics, theoretical computer science, machine learning, and other technical (or fun) topics, as well as writings on my personal experiences and reflections on research, learning and life in general.
Collaborative text editing with RGA
Notes on a tombstone-free RGA: proved RA-linearizable in Lean 4, then found to reorder your text on delete. Why convergence is not correctness.
LLM Proposes, Lean Disposes: A Week at the LeanLang Summer School
In July 2026 I spent a week at IISc Bangalore for the LeanLang Summer School, run by Emergence. Here is how I got there, what Lean actually is, why formally verified autonomy suddenly matters, and a tour of the week.
The Remarkable Theorem of Gauss
Gauss’s Theorema Egregium reveals that Gaussian curvature is intrinsic: it can be read from distances measured on a surface, without looking at the surrounding 3D space.
Hello, World!
·2 mins
Welcome to my blog! Here I’ll share notes on automated reasoning, formal methods, theoretical computer science, mathematics, machine learning, and more.