Leaving Berkeley

I’m leaving Berkeley soon. I want to share some fun moments from my time at Berkeley.

(pre-)First year

I started my PhD in Fall 2018. It is now Spring 2026, and you’ll see soon why it took me so long (you can probably guess if you’re Korean). Until my third year as an undergraduate, I hadn’t really thought about studying abroad. The major event that changed my mind was the Fields Undergraduate Summer Research Program, a summer REU at the Fields Institute in Toronto. I attended it when I was a senior, and it made me realize that I might be better off studying abroad and meeting more people in the world. But it was a bit late to apply for PhD programs, so I decided to do a master’s first at POSTECH. I applied to 15 schools (I wanted to apply to more, maybe around 30, but my English was poor and so was my TOEFL score) and got into Berkeley. The admission email ended up in my spam folder, and I found it a week after it arrived (so anyone applying to PhD programs or anything else: PLEASE check your spam folder).

I really enjoyed my first year. I took some courses and learned a lot (though I didn’t do well). My favorite class was David Nadler’s Lie Groups course, where he explained the subject in a very intuitive and geometric way. The exams were memorable too; they were all short-answer questions, and one of them gave us a list of 10 Lie groups and asked us to group them according to which ones shared the same Lie algebra (you can find it here). More importantly, all my cohort mates were really kind and very passionate about mathematics. Sometimes we would talk about math endlessly, and I was really happy about that. Also, Berkeley is close to San Francisco, so I could attend a lot of concerts, which was good for my mental health. I even went to a Muse concert once with a bunch of my cohort mates, though that one was actually in Oakland.

Alternative Military Service, Covid, etc

Unfortunately, I had to go back to Korea for alternative military service in 2019. Since I didn’t want to think about the qualifying exam after coming back three years later, I took it at the end of my first year. Berkeley’s QE is an oral exam where students choose three topics (two major and one minor), and I chose Automorphic Forms, Number Theory, and Complex Analysis (minor). I passed the exam, although I don’t think I did well in Automorphic Forms (my mind went blank, and I completely forgot how the Tate thesis and automorphic forms on $\mathrm{GL}_1$ work). You can find my QE syllabus and questions here.

After I came back to Korea, I started looking for a company to work at. For context, I (like many other people) had two choices: go into active military service (1.5 years), or work at a government-approved company for alternative military service (3 years). The first option is much shorter, but people often prefer the second because they can do something more interesting. I took the second path and eventually got a job at Riiid, an ed-tech company that uses AI to help students learn better (the company has since changed its name for reasons I don’t know). I worked there for almost two years, developing deep learning models for student performance prediction (usually called “knowledge tracing” in the literature) and recommendation systems. It was actually my first time learning about deep learning, and I learned a lot. It was also the era when BERT, GPT-2, Reformer, and others came out, and people were amazed. At the time, it was even possible to search for all ICML papers that used transformers and read all of them, or at least all the abstracts, which I did. Now that simply doesn’t make sense because every paper uses transformers. I also learned about reinforcement learning and Adam Wagner’s work on finding counterexamples to conjectures in graph theory using RL, which was the first paper I read on “AI for mathematics.”

I then moved to another company, CryptoLab. It is a very different kind of company, working on homomorphic encryption and applying it to private machine learning. I decided to move there because it seemed more mathematical, especially since homomorphic encryption (or lattice-based cryptography) is related to number theory. Eventually, I worked on developing a Python library on top of our homomorphic encryption library (called HEAAN, based on the CKKS scheme), which turned out to be mostly algorithm design work. In short, you have a limited set of operations on vectors of fixed length (component-wise addition and multiplication, and rotation), and you want to implement ML algorithms using as few operations as possible, especially multiplications and rotations. In some sense, I could do this without knowing much about the CKKS scheme itself, and luckily I was able to write a paper based on the work.¹

All of this happened from 2019 to 2022, which was also when the Covid-19 pandemic started. Sometimes I had to work from home, and it was not much fun since I couldn’t meet my colleagues in person. All the great gigs and concerts in Korea were cancelled. But anyway, things got better, and three years passed. The total number of days as a “professional research agent” (which is a translation of 전문연구요원, the official term for this alternative military service) was 1095, which is close to $1023 = 2^{10} - 1$. So I decided to buy a 10-disk Tower of Hanoi and take a picture of it every day, so that my service would end around the same time I finished the tower. You can find the pictures on this Instagram account.

Back to Berkeley, Strike, Thesis

I came back to Berkeley in Fall 2022. By then, all my cohort mates were in their fifth year, and I was the only one in my second year. The department was full of strangers, and honestly it was pretty lonely at first. Since I didn’t take any courses after coming back, I only attended seminars and mostly talked to the undergrads in my discussion sections. Since it was pre-ChatGPT, many students came to sections and asked a lot of questions, and I really enjoyed talking to them. BUT! there was a strike that semester, when graduate students and postdocs went on strike for better pay and working conditions. It lasted for about two months and eventually resulted in much better pay and many other benefits for students, but I was not able to finish my teaching or keep talking to the students. However, I saw some of them (three of them, to be precise) quite a lot over the remaining years, which was fun. Also, my friends found this and sent it to me, which might be the best achievement of my graduate student life.

I also had to decide on a thesis topic. My advisor suggested that I read Getz-Hahn’s GTM 300 book on automorphic forms and representations and try to find something interesting in it, so I did and found one topic: covering groups and the relative trace formula (the book itself has the subtitle “with a view toward Trace Formulae”, and actually it is toward Relative Trace Formulae). At some point, my interest shifted toward Ichino-Ikeda type conjectures for covering groups and exceptional groups. In particular, I read all four of Bhargava’s famous papers on higher composition laws, since they are closely related to automorphic forms on exceptional groups. More precisely, they give indexing sets of Fourier coefficients; for example, Bhargava’s cube is closely related to $D_4$ modular forms. Although I am not actively working on this now, I still have a long list of related problems, and I hope to work on them in the future. (Maybe some of them can be one-shotted by frontier LLMs…)

Sphere packing, informally

One of the biggest moments in my (math) life was Dan Romik’s talk on his new proof of the (quasi)modular form inequalities appearing in Viazovska’s paper on 8-dimensional sphere packing. I described the story in the introduction of my thesis, so let me keep it short here. In Viazovska’s paper, she constructed an (actually, the) optimal function for the Cohn-Elkies bound in dimension 8 using (quasi)modular forms, and the proof reduces to proving inequalities for certain quasimodular forms. She used interval arithmetic, and Romik found another proof using several modular form identities and their explicit values at $z = i$ (a special case of the Chowla-Selberg formula). He left the dimension 24 cases as an open problem, especially for graduate students, and I decided to give them a try. This was more interesting and harder than I expected, and I eventually finished it in summer 2024. At that point, I realized that there were many problems related to this, or more generally to positivity of quasimodular forms, and I decided to work on them for my thesis. If you are interested, you can find the details in my thesis. For now, there is another paper I uploaded to arXiv, and there will probably be two more (both incomplete in some sense, so I need to spend more time on them).

Sphere packing, formally

After I uploaded my paper to arXiv, Yaël Dillies found it and shared it on the Xena Discord server.

Coincidentally, Sidharth Hariharan was also on the server, and he had just started a project on formalizing Viazovska’s proof of the 8-dimensional sphere packing problem in Lean while he was an exchange student at EPFL. So he reached out to me, and I joined the project, along with Chris Birkbeck, Gareth Ma, and Bhavik Mehta. It was private at the time. Before we made it public at the Big Proof conference, we wrote some basic definitions and the statements of the main theorems, and we also polished the blueprint. After it became public, many people started to contribute, and many AI systems also started to contribute. The project then became famous for a reason that we didn’t expect, which also initiated a discussion about the role of AI in formalization. There are too many things to say about this, but I won’t repeat them here, and I recommend checking out Avigad’s essay as well as Lean Community Blog.² The only thing I want to repeat and emphasize is this: the project is not finished yet, and we (the maintainers) welcome all contributions (although progress has slowed down). You can find the project repository here, and a summary of the current state of the project in this paper.

Last semester

Spring 2026 was my last semester, and also the busiest semester of my life, since I had to write my thesis, teach, and do an internship at Axiom. I tried hard to find a way not to teach this semester so that I could focus on the other two, but I failed and ended up doing all three things, which made me extremely busy. Overall, I quite enjoyed working at Axiom, especially working with great colleagues including Ken Ono, Jujian Zhang, and Kenny Lau. The experience also made me think more thoroughly about the role of AI in mathematics, which I’d like to write a blog post about in the future (I already wrote one for young mathematicians, but maybe one more…).

It was also a semester that made me less interested in teaching, since many students were using LLMs for learning (and of course for doing homework… and even for cheating), and the number of students coming to sections was very small. I thought about this in the exact same way as I did in 2022, when I taught the same course, Math 53, and the attendance rate was around 40%. This semester it was less than 10%. One day, when there were only 4 students (out of 40), I actually asked them what made them come to section even though others were using ChatGPT to learn, and our conclusion was that human interaction is still important to them.³

When my internship and teaching duties ended, I had to focus on writing my thesis. At this point, ChatGPT and Claude helped me A LOT, especially with fixing my poor English, but also with finding some mathematical errors. Most importantly, I (or everyone who graduated this semester) had to meet the accessibility requirement for the thesis, i.e. make the PDF file more accessible by adding metadata and tagging. I learned that it is very hard to do this in TeX (other departments write theses in MS Word), and every single math graduate student graduating this semester had the same problem. Eventually, I used Codex and Claude for days to add some TeX options that I still don’t fully understand, but they resolved all the issues flagged by Acrobat Reader’s accessibility checker, and I was able to submit my thesis successfully. Thank you, AI!

What’s next

During the summer, I’ll be in Korea except for one week, when I go to ICARM for a workshop. There are a lot of workshops and conferences on AI for mathematics coming up, and I’ll be attending several of them.

In Fall, I’ll be in Switzerland, and probably staying there for at least a year. I don’t know yet what I’ll be working on. But I’ll do math, write Lean code, and explore AI, among other things. I hope it will be fun.

Tags: math