A Universe of Sorts

The lives of Udupi-Ajja and Huduco-Ajja, written down before the details fade.

A year of SAT solvers, UNSAT proof calculi, and bitblasting for Lean, as my research group moved from Edinburgh to Cambridge.

On binge programming versus the steady drip of research, and what it took to move from one mode to the other.

First year of the PhD: giving MLIR a semantics in Lean, moving from India to Edinburgh, and learning what a PhD even is.

Harish carves wood close to home. On caste, craft, and skills learnt by practice from birth that he holds cannot be taught.

How this blog compiles math to plain HTML at build time with a thousand lines of C++ - no MathJax, no client-side rendering, instant loads.

Papers, books, and ideas that survived a year of lost data - the memorable remainder of 2019.

A future history of geometric computation theory: billiard balls on symplectic manifolds, and the fall of the EDA industry.

A future history of type theory: logics of relations, prolog-like computation, and topology coming online.

Analysis feels like algorithms, algebra feels like data structures: midnight discussions with my room-mate about mathematical taste.

Abstract interpretation looks magical on paper; in practice, widening is a black art. Notes from trying to use it on real code.

A tensor is a collection of numbers that track something physical, explained with a deque.

Non-strict evaluation explained for C programmers, down to how graph reduction runs on stock hardware.

The p-adics by analogy: primes as points, integers as polynomials, completions as Taylor expansions.

Grobner bases as confluent rewrite systems for polynomial arithmetic, with a worked application: computing equivalent gate sets.

Entropy as expected surprise, entropy as bits you have to pay, and KL divergence as the extra bits an encoder wastes by assuming the wrong distribution.

Simplicial homology for anyone with linear algebra and group theory: detecting holes with pictures, without the machinery of algebraic topology.

Open sets are semi-decidable properties and continuity is computability: topology re-read through Escardo's synthetic lens.

The humble triangle again, now with functions living on it: cohomology as the linear-algebraic dual of homology.

Sheaves, topoi, geometry, and logic - writing down what I understand to find the relationship I don't.

The reference word2vec implementation does not do what the paper --- and every explainer of it --- says it does.

Bitwise AND on the 2-adics defines the naturals, and Hilbert's 10th makes the theory undecidable.

Sonatas, pop covers, and jazz: a living list of what I'm playing and listening for at the piano.

A living list of what I read and want to read: weird literature, hard sci-fi, ergodic fiction, and the rest.

Recipes I actually cook, rava dosa onward, written down so I stop reinventing them.

Quotes I keep returning to, from Breiman on theory versus inquiry to the Seikilos epitaph.

Paintings, illustrators, and pieces I love: Hiroshi Yoshida, Klimt, and company.