§ Stuff I learnt in 2024

• Quick TL;DR of the year: My research group moved from Edinburgh to Cambridge, so I was looking forward to lots of courses to take!
• I'd also settled in on an area I wanted to work on for my PhD, which was to design, implement, and verify the correctness of decicision procedures for the Lean theorem prover, which guides much of the reading I've done.

§ Resolution, UNSAT proof calculi, Bibtlasting

Much of this stuff was learnt in many discussions with my friend, Henrik Böving . I had a lot of fun studying the theory of SAT solving and their UNSAT proofs.

§ UNSAT proofs

• Resolution is refutation complete, a clean proof . The proof is purely constructive, and gives a nice intuition for how resolution "works".
• Hyper-resolution: This is a cool proof system that is stronger than resolution, and whose completeness properties implies theorems like the nullstellensatz! I learnt of this from Semantical Completeness Theorems in Logic and Algebra .
• The Potential of Interference-Based Proof Systems by Merijn Heule and Benjamin Kiesl. This is a really interesting paper, which explains how proof systems that involve rules with the global set of clauses, that can "interfere" with each other can give rise to more powerful proof systems.
• Lower bounds on resolution proofs , No known lower bounds on extended resolution proofs .
• I read quite a lot of the source code of Bitwuzla , a state of the art SMT solver for bitvectors, arrays, uninterpreted functions, and used its encodings for the formally verified bitblasting circuits in Lean.

§ Interpolation and Model Checking

I found he idea of interpolation based model checking to be extremely cool.

• Craig interpolation is a fundamental technique, which when given formulae $A$ and $B$ such that $A \implies B$, builds a new formula $C$ such that $A \implies C$ and $C \implies B$, furthermore, $C$ has variables that occur only in both $A$ and $B$.
• Interpolant based model checking , which is a really cool paper that showed for the first time how one can use interpolants to compute inductive invariants for model checking. I found the idea to be super clever, and also the idea of using interpolation as an "extrapolation" between the current step and the next step was super kawaii.

§ Writing a SAT solver

I've been implementing a SAT solver over at bollu/casette by following the MiniSAT paper , and it's been super educational.
In general, it turns that implementing the core of a CDCL based, incremenetal SAT solver doesn't need too much! It needs some careful data structure engineering for doing efficient trail management and unit propagation, but other than that, the rest is quite straightforward.
I wasn't able to find a correctness proof for the calculation of the first UIP in the MiniSAT paper, so I wound up writing the prof down. The key insight is that given a DAG with a source vertex, the dominator of the sink vertex can be found by visiting nodes in reverse BFS order. The key invariant is that when visiting nodes in reverse BFS order, a node $p$ (parent) is visited only after all of its children are.

§ Other Decision Procedures

When interning at AWS, I got to talk to lots of fantastic folks, including Shilpi Goel , Jim Grundy , Leonardo De Moura , Kim Morisson , Nathan Wetzler , John Harrison and many others, who gave me lots of pointers to really interesting ideas many of which I'm yet to read. I list them down here:

• Tarski's quantifier elimination for real closed fields
• Cylindrical algebraic decomposition for deciding real closed fields.
• Quantifier Elimination in p-adic Fields , which surveys decision procedures for deciding the first-order field theory of the p-adics.
• Model based algorithms for UNSAT of LIA: Cutting to the chase .
• String Solvers for solving string constraints. I started reading the theoretical landscape here, and it seems to be super weird --- in particular, we don't even seem to have a clear computability theoretic understanding of strings plus integer solvers!
• Shannon encoding for solving XOR constraints
• Automating decidability of linear integer arithmetic with divisiblity constraints with Grobner Basis . More generally, HOL light has lots of solvers that we need to steal into Lean!
• Exists-forall solvers by model-based generalization.
• Reed Muller expansion and XOR-based normal forms

A good reference for at least some of these appear to be the course Little Engines of Proof .
There are many more decision procedures I want to learn, mostly coming from algebraic number theory, algebraic geometry, and 3-manifold theory. Many of these are not critical to my day-to-day for the next year, but I consider it important that I know them, and so I list them out here.
A good reference for some of the algebraic and number theoretic ones is Computational Algebraic number Theory by Henri Cohen. The SnapPy project for 3-manifold algorithms has lots of super interesting algorithms for deciding facts about 3-manifolds. Since knots can be identified with their knot-complement, and apparently, the knot complement can be given a 3-manifold structure, it also provides decision procedures for knot. I realized that I need to know a lot of 3-manifold theory, so a current medium-to-long-term wishlist maths is to study Thurston's geometry and topology of 3-manifolds . To be extremeley honest, if it is possible, I am tempted to spend a semester at the Indian Institute of Science reading through the book with Siddhartha Gadgil's supervision, if he's interested to let me take this on.

§ Cambridge Vibes: Lectures and Reports

• Descriptive Complexity , a course taught by Anuj Dawar , about capturing the power of different complexity classes by different logics. It was a really cool course, and I learnt a bunch of uses for game semantics from it! I would love to spend more time thinking about this stuff.
• Denotational Semantics by Meven Lennon-Bertrand . I loved the course, but I only attended sporadically. I've seen the material before, so I wanted to take it for review. Asking meven questions was always enlightening, and I learnt a lot from the many hallway conversations I've had with him, including a clarification of what the hell proof by reflection does.
• To write my first year report, I wound up doing quite a bit of survey on verified compliation, proof by reflection, and decision procedures. I'm going to only list the most salient bits here: (i) CakeML, (ii) ACL2 and its proof by computation, without dependent type theory.

§ Projects for Master Students at Cambridge

• A=B is a decision procedure for deciding equalities of combinatorial recurrences. I'm supervising Ben Przybocki , who's implementing Sister Celine's algorithm in Lean .
• Solving Exists-Forall problems with Yikes : We'll be using the algorithm to implement a formally verified version of John Reghr's recent work via HYDRA: synthesizing peephole rewrites
• Adapt SAT based sudoku solvers to use color constraints . Humans who solve sudoku have come up with a paradigm shift, where one can use colors to make certain 'symmetry arguments'. I would be interested to extend a CDCL SAT solver to propagate such color constraints! The inspiration: The Miracle Sudoku, of solving a suduko-like with a single solution .

§ Optics and Photography

My friend, Anton Lydike has been encouraging me to pick up photography, so I wound up doing that this year. I first began by learning about shutter speed and exposure, by reading the books:

• Understanding Shutterspeed: Action, Low-Light and Creative Photography, and
• Understanding Exposure: How to Shoot Great Photographs with a Film or Digital Camera.

However, it wasn't clear to me that I actually understood what was going on, so I wound up writing a raytracing simulation for classic geometric optics to understand these phenomena, over at bollu/optics . It was a really good exercise to both refresh my memory of raymarching, but also to setup scenes where I could understand what e.g. focal length and aperture did to the final image, as a function of incoming light waves. I'd highly recommend such an exercise to get a felt sense. The simulation was written in C++, with raylib as the GUI library. Raylib's a blast to work with, and was super enjoyable to write code in! However, I think I like egui better, cause it's just much more fun to write Rust, and it's API is so much more ergonomic. Regardless, Link to the simluation video .
Next, to learn how to actually edit photographs, I've been reading the darktable user manual , which has lots of good information about the algorithms used for image processing. I enjoy their random asides, such as the whole tirade about [scene referred versus display referred workflows ]. TL;DR: Display referred assumes that light intensity can be normalized between $[0, 1]$ before starting processing. On the other hand, Scene referred only normalizes at the end, and thus light intensity live in $[0, \infty)$. I don't understand at all why the normalization is incorrect, so if someone wants to educate me, please do leave a comment below. Even so, I enjoy the sheer opinionatedness of it all.
Anyway, I plug my DeviantArt here, so give a follow if you like!

§ Music and Composition

Unexpectedly, in the middle of a year, a friend ( Luisa Cicolini ) mysteriously got me back to playing the piano through no fault of hers. This led me to read quite a lot of compositional theory, music history, and counterpoint.

• A Natural History of the Piano , which is a funny, pop book on the history of both the instruments and the artists. I enjoyed reading it, since I definitely was unaware of a bunch of the history of the invention of the piano.
• Johann Joseph Fux: Study of Counterpoint , which provides a socratic description of how to compose in counterpoint. I'm still working through the book, but doing the exercises has been a blast so far.
• Open Music Theory , an open textbook for
• Ragtime music theory appears to be much less well-developed. I would love to have pointers on how to compose ragtime, since I feel that even today, I cannot personally compose something as genius as Maple Leaf Rag by Scott Joplin , as it's super harmonically dense. If someone has pointers, please drop me a message!
• Harmony, Counterpoint, Partimento: A New Method Inspired by Old Masters , where Partimento is a technique that's used to improvise in the old Renaissance style. I've been having a lot of fun studying and practiscing partimento theory.
• Literally everything that Glenn Gould has ever said , since I consider the man to be a genius. He was a strange musical savant, who had lots of entertaining opinions, such as the fact that "Mozart became a bad composer because he was so good at improvisation!"

Toward this time, I also got interested in explanations of Jazz (a)tonality, so I went and asked Alan Blackwell , who is a Professor of Interdisciplinary Design about where I could study such a theory. He pointed me to work by Dmitri Tymoczko, called The Geometry of Musical Chords , where one uses orbifolds to represent the tonnetz . This also led me into reading more about atonal music composition, and in particular, the twelve tone theory by Schoenberg . While I'm not a huge fan of the music, I can at the very least, understand what it's trying to do now!

§ Monodrone

In a fit of insanity, I decided that I wanted to precisely understand how a tracker such as MilkyTracker worked, so I decided to write one myself. However, I hate debugging off-by-one-errors, and so, I decided to formally verify the whole thing in Lean instead. This lead to bollu/monodrone , where the core tracker data structure was written in pure lean4 , with a rust ffi , and a cargo build script to smash Rust and Lean together, and a egui-based UI for rendering. This was quite fun, and I managed to snipe a friend, Sébastien Michelland to write an alternative Coq formalization that he felt was more elegant.
Moreover, I wound up extending it with a chord recognition algorithm , since I was trying to think about chord inversions and extensions in the process of getting back to piano. This was a wild ride, because it seems that the state of the art is to make gigantic tables ala Music21, which is based on Neo Riemannian / Tonnetz based chord naming conventions, or to use atonal music theory See Alan forte: The structure of atonal music . I disliked both ideas, and instead just wrote something that brute forces all possibilities and ranks the outcomes based on a vibes-guided heuristic. It works well enough that I'm happy with it!
The funny thing was, while I did this purely for recreation, having thought about deciding the overlapping of 1D contiguous segments of notes turned out to be exactly what AWS wanted me to do, except one replaced "notes" with "memory regions"! This just got me even more convinced that no screwing around with code is ever wasted.

§ Shakespeare

I've always wanted to enjoy Shakespeare's works, and school sadly failed to impart any enjoyment of this to me. This year, I got two opportunities to learn more about Shakespeare. Firstly, there was Shakespeare in the summer , which is a Cambridge event where lots of shakespeare plays are put up by theater troupes. My friend, John Mark Poole, took me to a bunch of these, and kindly explained to me both the historical context, as well as gave me a sense of how I ought to watch, compare, and contrast the different interpretations of the same play. I had a lot of fun with this, and I can definitely say that I enjoy shakespeare now! Secondly, I watched the Shakespeare lectures by Marjorie Garber with my ex-partner-and-still-amazing-friend Sahiti , which was a blast, since they're way better at this language stuff than I am. I personally found watching different interpretations of Macbeth to be super interesting, since Macbeth can be played as either tragic or as malevolent, and this totally changes the tenor and arc of the entire story.
Overall, I'm really happy that I learnt how to enjoy Shakespeare this year, and I'm looking forward to continue to engage with more of the canon next year.

§ Poetry

I spent a bunch of time this year trying to find poetry that I actually liked, or to give up on the aesthetic project known as liking poetry. I started from what I knew I actually liked, such as Shelley and Tennyson, and then attempted to speedrun the next couple centuries of poetry history. To do this, I would up watching lectures and performing background reading on literary critism. In particular, the lecture series Introduction to the theory of literature by Paul H Fry was instrumental in this. The lecture series covers the evolution of literature, poetry, and critiques of these by their respective communities. This actually gave me lenses to understand why I should even bother caring about Auden, for example. Paradoxically, this and surrounding reading made me dislike modernists even more --- A single useful article was What is New formalism by Marjorie Levinson, which lays out the new formalism manifesto, which made me realize why I dislike most of the formalist 20th century poetry in the first place! Anyway, I wound up collecting a bunch of poetry I do in fact like:

• Rebel Angels: 25 Poets of the New Formalism
• Poems by A.E. Stallings and in particular, Ajar :

Ajar by A. E. Stallings
The washing-machine door broke. We hand-washed for a week.
Left in the tub to soak, the angers began to reek,
And sometimes when we spoke, you said we shouldn't speak.

Pandora was a bride; the gods gave her a jar
But said don't look inside. You know how stories are—
The can of worms denied? It's never been so far.

Whatever the gods forbid, it's sure someone will do,
And so Pandora did, and made the worst come true.
She peeked under the lid, and out all trouble flew:

Sickness, war, and pain, nerves frayed like fretted rope,
Every mortal bane with which Mankind must cope.
The only thing to remain, lodged in the mouth, was Hope.

Or so the tale asserts— and who am I to deny it?
Yes, out like black-winged birds the woes flew and ran riot,
But I say that the woes were words, and the only thing left was quiet.

• One Robe, One Bowl: The Zen Poetry of Ryokan

The theif left it behind—
the moon
At the window

Today’s begging is finished; at the crossroads
I wander by the side of Hachiman Shrine
Talking with some children.
Last year, a foolish monk;
This year, no change!

Twilight, --- the only conversation
on this hill
Is the wind blowing through the pines

• Poetry by Vladimir Nabakov . I really enjoy his poetry, since it's generally clever, witty, short, and rhymes, which makes it perfectly the type of thing I want to memorize. An example poem of his, "To the Grapefruit" which I did memorize (thereby completing a life mission of memorizing poetry):

To the Grapefruit by Vladmir Nabokov
Resplendent fruit, so weightly and so glossy,
exactly like a full-blown moon you shine;
hermetic vessel of unsweet ambrosia
and aromatic coolness of white wine.

The lemon is the pride of Syracuse,
Mignon yields to the orange's delights,
but you alone are fit to quench the Muse
when,thirsty, she has come down from her heights.

I memorized "To the grapefruit" as a personal challenge to myself, and that was a really fun exercise! I'm glad that it's now with me, forever. It feels similar to learning proofs, to be honest, and I seem to bring it out and turn it in my mind as often as I do a pretty proof. I'm considering memorizing "Lilith" next, and I'm open to suggestions for somewhat-short, rhyming poems that are very, very clever.
Next year, I want to continue my quest of reading more "epic poetry". I read the divine comedy and Beowulf last year, and found it to be a lot of fun. This year, I have some more listed out, from different cultures. I don't know if I'll be able to find translations, but that's half the fun! Tain bo Cuailnge , aka the irish illiad, Beowulf: A new verse translation by R.M. Liuzza , Kavevala, which is finnish epic poetry , and Nibelungenlied, an epic poem in High German .

§ Other Reading

• A Year in the Life of a Shinto Shrine : Really meditative book on an american family that goes and lives at a shinto shrine. I only half-completed it, but I really did enjoy the meditative pace of the book.
• Imaginary Museums: Stories
• The Name Of The Rose by Umberto Eco
• Serendipities: Language And Lunacy by Umberto Eco
• Man and his symbols: Jung . I reread parts of this book most years, and this year was no exception. I wound up returning to it because of the weird studies podcast discussions on Tarot. I like living life based on vibes, and so Jung is peak how-to-live-by-vibes.
• Suture disturbing, well written body horror.
• Brothers Karamazov by Dostovyesky , which I bounced off of halfway, because it felt like it couldn't decide if it was a philosophy book or a novel.
• Marco Valdo by Italo Calvino , which felt like invisible-cities-lite, with short slice of life stories, all of them surreal.
• The Divine Farce , which explores the meaning of life in the most horrible parable possible.
• A short stay in hell , which is a meditation on what the Library of Babel would be like if meted out as punishment. Once again, horrible story, would recommend.

§ Plans for Next Year

• Implement all the decision procedures! But really, I want to polish up Lean's bitvecotr support till we have formally verified versions of the commonly used tools in the LLVM community, following which I shall write either solvers for LIA, or for strings.
• Take the number fields course at Cambridge, since in trying to read the textbook 'computational algebraic number theory', I realized that I know less algebraic number theory than I would have liked.
• Learn engineering drawing: This has been a lifelong goal, since I really enjoy architecture, but this was boosted up the priority list when I asked Keenan Crane how to learn to make pictures like his, and he recommended that I pick up engineering drawing. A cambridge professor, Nathan Crilly , kindly offered to help me self-study, so that's what I'll be doing!
• Get good at blues scale playing and counterpoint composition + improv: I find counterpoint to be really really satisfying to listen to, so I'd like to spend some serious time getting good at improvising counterpoint! Apparently, mozart used to be able to do it, so why not me :).

§ What does the year feel like?

Overall, it was a really fulfilling year. I found out what I really want to do for my PhD, for real for real this time: Implement and verify decision procedures. It fits exactly the kind of person I am: I enjoy thinking deeply about algorithms and proofs, and implementing kawaii cores with lots of surrounding heuristics to make stuff go fast! I'm super excited for 2025, because I feel like I've finally found product-market fit for my problem statement.
It was a sad year too, 'cause I broke up with my long term partner. I'm optimistic that we'll remain close friends, as we were before we began dating, and I am super excited to see what they do next!
Cheers, and let me know what I should read, try, and do for next year. After all, New Year's resolutions are still a day or two away!