It's August 30, I'm stuck in a hotel room in Ann Arbor while running a long simulation, and I thought now would be a good time to recap on my summer. I didn't go into this summer with any plans - I didn't get into any of my REUs, I had 0 internships lined up, and I had a lot of time to myself. To be honest, after a really busy semester I didn't really know what to do with all the time I was given. It took me some time to orient myself towards doing projects again—not that the projects weren't fun, but I wasn't used to having both free time and energy at the same time. I spent the first month or so of my summer just hanging out with my friends, getting lunch or dinner together in the city, and not doing anything particularly important.
I think the first project I worked on was this Laplacian eigenvector visualizer. I saw some people on Twitter talking about Sheaf Neural Networks, which led me to Graph Neural Networks, which led me to the Laplacian matrix of a graph. Put simply, the Laplacian of a graph is a alternative representation of the graph (as opposed to the adjacency matrix) which helps with intuiting flows on the graph. A function on the vertices of a graph is a weighing of graph nodes, or a vector. Then applying the Laplacian to this vector gives you a new vector, which tells you (roughly) how much bigger your original vector's values were at a node than its neighbors. It's easy to see that is an eigenvector for any Laplacian matrix, but as it turns out, the second eigenvector (ordered by eigenvalue size ascending) gives a partitioning of the graph which is a good approximation to its sparsest cut. I had a hard time visualizing what such a vector would look like geometrically (? or, graphically?) so wrote a simple Three.js app where I could construct graphs and label their nodes based on the eigenvalues of their Laplacian matrix. I didn't know any Three.js going in so most of the app was generated by 4o (can I even call it my project atp?), and it took about an evening to write from start to finish.
Over the spring semester, I became really interested in Furstenberg's proof of Szemerédi's theorem. It's a really interesting proof that spawned a subfield of Ergodic Theory methods for proving combinatoric results—I found this Chicago REU paper to be a really good intro. I also gave a talk on the proof. Semi-tangentially, at the start of the summer I joined a twitter group mainly discussing Haskell, but also other functional programming languages. One of these languages was lean. This was also around when LLM-based AI theorem provers in lean were going viral on twitter and Terence Tao started posting lean tutorials on youtube, so I knew I wanted to learn lean. I decided on formalizing Furstenberg's proof in lean as a first project. Unfortunately this was a pretty ambitious project and was a bit doomed from the start: This was my first lean project, some people in the community had already decided against formalizing Furstenberg's proof because it would require formalizing a lot of measure theory and ergodic theory first, and I was just an undergrad who had only a practical understanding of measure theory. Working on the project took the form of a lot of sorrys, a lot of swearing, and a lot of arguing with 4o, and I lost steam after a few weeks. To this day I'm not sure I can say I "know lean." But I did gain some opinions on lean, theorem-proving using AI, and language design through the project so I would say my time was well-spent over all.
Around the time I stopped working on the Furstenberg proof, I picked up a copy of The Implementation of Functional Programming Languages by Simon Peyton Jones from a used bookstore in San Jose. (If you ever find yourself in South Bay and you love computer science textbooks, this is the place for you!) I had a big picture understanding of how imperative languages like C or Java were compiled into machine code, but I've always wondered how functional languages, whose program structure were so fundamentally different from machine code, were compiled. The book follows the compilation process of Miranda (a predecessor to Haskell), from parsing to type checking to compilation into G-machine instructions and more. I also followed along with my own implementation of a toy functional language, and I used the project as an opportunity to write Rust. Picking Rust back up wasn't too difficult and I was able to write a parser and a type checker, but some other responsibilities (which I will talk about later) unfortunately caught up to me and I haven't gone back to it as of writing. I think I got pretty good at writing parsers quickly (although I don't know about performance), and I now understand what people mean when they talk about System F or lazy evaluation.
There are a few other things I've done on the side. In late May I started collecting facts about most real numbers. This was originally inspired me learning about fat Cantor sets from my old ergodic theory DRP advisor, and I've since been interested in the idea that there are properties that most real numbers, but not necessarily all of them, possess. I've done a lot of searching and have gotten some contributions (thanks, Nick!) since then, but I'm still on the lookout for any other properties of most real numbers. Another mini project was resurrected by me finding an old file in my home directory that I'd abandoned—a bitmap video of Bad Apple I'd intended to use for an edit. I ended up making this out of it. I also read a few books this summer. I finished reading The Master of Go by Kawabata, which I really enjoyed. Then, I read The Face of Another which I also found interesting (I read the first bit of it in high school for a translation class, but never got to finish the rest of it)—this one I think Nick will like. Recently I started reading The New Science of the Enchanted Universe, which I mainly interpret as a fleshing-out of the same ideas in this substack article about cargo cults. I really liked the first chapter, but the second chapter on feels a lot like bug-collecting so I'm not sure I'll continue it. The ideas around theological frameworks as technologies is really thought-provoking, though.
Since the beginning of July, I've been working for Complabs, a company building AI for setting up mechanical simulations. It's been a blast working on this problem, and it's taken up the majority of my time since then. I've recently decided to take a year off from college to work full-time for them. I see my decision as a calculated bet on myself. I'm not used to betting on myself, so this is obv a very scary situation for me. (I also don't idolize dropping out, unlike some people.) But I'm excited about being able to build things and I'm hoping to learn a lot in the months to come.