It's been a while since I last published a post here. In fact, my bio was still saying I'm 18 before I changed it 😂​ Here's an update! A lot of exciting projects.

I gave a talk at Imperial! It was part of the "Warwick IMPerial mathematics conference" (WIMP). Despite Warwick only being 25% of the acronym, we still had 4 (out of 9) speakers presenting late-undergraduate level Mathematics. My talk was on analytic number theory, specifically an introduction to sieve method and the circle method. The slides can be found at https://github.com/grhkm21/wimp-2024/blob/master/main.pdf. The talk is inspired by Travor Liu's amazing blogs on analytic number theory.

I am currently formalising a recent (2020s) result from extremal combinatorics in Lean, a Mathematical theorem prover, under the supervision of Damiano Testa for my third year project. It has been around a year since I started formalising Maths in Lean, and I find it really interesting, as I get to think about Maths quite differently. The code can be found on my GitHub https://github.com/grhkm21/lean4. There's also a private repo that I will make public when the grading is over in May :)

As a side project, I have also been assisting with the Prime Number Theorem project (to achieve the exp-root-log error term), started by Terence Tao and Alex Kontorovich. I proved one tiny corollary in three days, so that's some progress... My fork of the repo can be found https://github.com/grhkm21/PrimeNumberTheoremAnd.

I had the opportunity to two cryptography events, Sage Days 123 (isogenies in Sage) at KU Leuven and UK Crypto Days at Bristol. I am writing blogs for both events and they'll be published on https://b6a.black/ "soon", so I won't go into much details here. TL;DR I met a lot of cryptographers 😀

Finally, I have been learning more Maths (as usual) in my free time. Recently I'm into some [co]homology theory, some algebraic topology and adjacent theories. Hopefully I will get a more in-depth understanding of it.

I am cooking a few more projects and they'll be public in the next few months. In the meanwhile, here's a page in my Lean formalisation notes. You might notice they are quite elementary, but breaking down a proof into such elementary steps is very important in proof formalisation.

:wq

Hi! As some of you know, I have been working on lattice cryptography the past three months, (formally) ending in two days! It has been an amazing journey and I gained a ton from this experience. (That sounds like a LinkedIn post, sorry.) I will write a full update soon, but here's a preview on what I have been up to during this period!

Btw I love the reindeer soup and salmon soup here... sooooo good.

Note: If this looks like astronomy rather than crypto, you are half-correct LOL