From March to around mid-July 2023 I worked on mathlib4 – more specifically the porting of mathlib, the ultimate evolution of Euclid's Elements, to the corresponding version of the Lean theorem prover. I was exposed to most of the maths I already knew from my double-degree university education and my self-learning, and then some, while (mostly) transcribing code to the new Lean version entirely out of my own free will and spare time.
I found a lot of friends on the way, the big-name mathematicians who maintain different parts of the Lean ecosystem. My passion developed almost to the point of addiction – I had truly found paradise – but the fanaticism had to end somewhere, and it ended when the port was officially declared complete on 16 July.
This picture is my personal tribute both to the gargantuan porting effort (over 1 million lines of code subject to continuous integration) and the people behind it including myself. The Lean code in Hearth Taxel's monitor is from my PR #6060.
