Harisankar B
Research student at NISER
Theoretical Computer Science | Formal Methods | Logic | Machine Learning
Recent
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
·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.
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.