Introduction
The prominent British mathematician G. H. Hardy (opens new window) (1877-1947) said he had never done anything useful in his life. But don’t judge him. He did many wonderful things but is somehow, unfortunately, most famous for his discovery of Srinivasa Ramanujan (opens new window) (1887–1920). Hardy was a number theorist, and number theory is considered by many as the queen of mathematics. Carl Friedrich Gauss (opens new window) (1777–1855) once said: “Mathematics is the queen of the sciences and number theory is the queen of mathematics.”
Well, for a long time, number theory was pure mathematics. But times change. No mathematician in the 1940s could imagine that in a couple of decades some highly advanced and abstract mathematics discovered in one of the French military prisons would be used by pretty much everyone on the planet. And yet it is so. André Weil (opens new window) (1906–1998) refused to serve in the army during World War II and was put in prison in 1940. This is where he made some of his most important discoveries. The work was about pairings (opens new window), and today pairings are used heavily in computer security, more precisely – cryptography. By the way, Weil famously said that every mathematician should spend a couple of years in prison.
And that’s actually what fascinates me the most – mathematics that used to be considered pure and looked like it could never be anything but pure, subsequently turned out to have unexpected applications.
I had ups and downs in my relationship with mathematics. I was a lousy student for most of my years at college and I didn’t touch mathematics for quite some time after I graduated. However, the desire to learn now seems to be getting stronger every year.
But what is it that I would like to learn? Some years ago, my wish list was something like:
- Understand the mathematics behind Weil pairing.
- Understand the proof of Gödel incompleteness theorems.
- Learn how to use Lean to verify nontrivial proofs.
- Understand how homotopy type theory is used in formal verification in mathematics.
This list changed a lot when I somehow unexpectedly began working in Web3 cryptography in 2021 and commenced my PhD in isogeny-based cryptography in 2022.
The first item remains valid, and I still intend to read The arithmetic of elliptic curves (opens new window) by Joseph H. Silverman page by page at some point. Currently, I occasionally read sections of it.
For the second point – Gödel’s proof left me speechless; it is so very different from anything else I’ve seen in mathematics. That said, I doubt I will continue studying logic; it is incredibly fascinating but also somehow disconnected from other areas of mathematics. On the other hand, in Paul Halmos’ wonderful autobiography (opens new window), I’ve read about how he handled logic with algebraic structures. Sounds interesting, but I am not sure I will ever explore that.
Studying Gödel’s proofs actually led me to the lambda calculus, which finally brought me to the third and fourth points of the above list. The third point is about how to verify proofs using a computer. And that is totally exciting. The math that is used to enable such verifications seems to be crazy difficult and beyond exciting. Sadly, I’m only able to use Lean (opens new window) for very simple proofs; anything nontrivial is beyond my reach at this point. And I haven’t touched it in a long time, so I might have already forgotten most of what I knew.
I am no better at the fourth point either. I have no idea about homotopy type theory. This one was actually the longest shot by far. I started studying Topology (opens new window) by James Munkres, Lambda-Calculus and Combinators (opens new window) by J. Roger Hindley and Jonathan P. Seldin, and Type Theory and Formal Proof (opens new window) by Rob Nederpelt and Herman Geuvers – to pave the way for me to understand homotopy type theory. But I’ve given up on this one. Too little time, too much of something I know almost nothing about.
Now I am primarily studying isogeny-based cryptography and the zero-knowledge proofs and their applicability in Web3. Yes, it’s pretty much about applicable math (sorry Mr. Hardy), but it’s incredibly broad and beautiful nonetheless.