Harisankar B

I am a fifth-year Integrated MSc Mathematics student at NISER, with a minor in computer science. I work on formal verification and automated reasoning: writing machine-checked proofs in Lean 4 and asking what it takes to trust a piece of software.

Most recently I was a research intern at FP Launchpad, IIT Madras, with Dr. KC Sivaramakrishnan, verifying replicated data types for distributed systems. Before that I spent a summer on logic and automated reasoning at IMSc Chennai with Dr. Meena Mahajan.

Research

Research interests, internships, and publications.

Writing

Notes on mathematics, CS, and proof assistants.

About

Background, interests, and contact.

Recent

Collaborative text editing with RGA

30 July 2026·24 mins

Notes Lean Formal Verification CRDT Collaborative Editing Distributed Systems

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 July 2026·14 mins

Notes Lean Formal Verification Theorem Proving LLM 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

16 May 2026·6 mins

Mathematics Differential Geometry Gaussian Curvature 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.