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.
Distributed Systems
LLM Proposes, Lean Disposes: A Week at the LeanLang Summer School
·14 mins
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.