FA+
Shop
From port to PhD
3 months ago
In February 2023 I had been out of university for seven months, having obtained two bachelor's degrees – one in mathematics and the other in computer science – but I was working as a lowly data analyst for SMRT Corporation, one of the two train operators in Singapore. Although I wasn't held to strict performance standards and I was otherwise comfortable in my cubicle, I felt bored with the few tasks I was assigned, tasks that barely stimulated my brain or required me to draw on the depths of knowledge I accrued over five years of studying.
I began drifting around GitHub and the Stack Exchanges, looking for more interesting things to do. Then I stumbled on the software system that would change my life forever.
The Lean theorem prover. A programming language for formal verification, something I had dabbled in in a few undergraduate modules as well as my internship and final-year project – but with a promise of being infinitely more expressive and intuitive than the SAT solvers I worked with. At the time I joined the project the community was porting Lean 3 to Lean 4, and they were pleading for volunteers to port thousands of files of mathematical theories formalised in Lean 3 – so I jumped right in.
Soon enough I couldn't stop. Not only was I reserving entire trees of files to port and working much faster than other volunteers, I was learning the language at a far deeper level than could be achieved had I gone through textbook-style resources like the Natural Number Game. Then I got my own ideas of new theories to formalise directly in Lean 4, such as Turán's theorem and Abel's limit theorem.
The port to Lean 4 officially ended on 16 July 2023, and I spent the next year doing low-level stuff in Lean. That ennui ended when the Carleson project was started to formalise one of the hardest proofs in mathematics. Its tasks were very appealing to me, not requiring many new definitions and proofs to be hammered out, but rather a long string of bound computations involving basic measure theory and combinatorics. I ended up formalising a great deal of tasks there (up to and including the time of this journal).
Around the same time I was interested in contract bridge and riichi mahjong, and would sometimes use my SMRT staff pass (doubling as a free travel pass on all Singaporean public transport) to go to NUS for student-run game nights for those two games. On one such occasion I met another undergraduate and learned that he lived very near my own house, and when I told him about my prior studies he asked me if I was going to return for Masters or PhD.
At that point I was seized by the realisation that my Lean experience was my ticket back to university. I began frantically searching NUS's computer science professors and my former lecturers for referrals, eventually settling on Ilya Sergey as my preferred PhD advisor (it is possible to skip masters and go directly to PhD, as happened here). I started my application for PhD in October 2024 and submitted it about a week before the deadline in early November 2024.
Through the new year and into February 2025 I began being contacted by AI companies using Lean, offering me contractor work while I was waiting for my application results. I applied for and was accepted into two such positions (though I soon forgot about one of them because they weren't holding me to anything and were paying significantly less than the other company). And then, on 25 April 2025, I got the massive news – my PhD application had been accepted and I would start on 4 August 2025.
That would of course require me to resign from SMRT, and I have done that. Considering everything, though, SMRT supported me well throughout these three years, providing me with some train-related coding problems yet leaving enough free time to pursue the interests that, in a merry and colourful way, led to me landing the PhD programme. For this I shall always be grateful, and I look forward to a future where I can really put my knowledge at the service of the world.
Jeremy Tan / Parcly Taxel
I began drifting around GitHub and the Stack Exchanges, looking for more interesting things to do. Then I stumbled on the software system that would change my life forever.
The Lean theorem prover. A programming language for formal verification, something I had dabbled in in a few undergraduate modules as well as my internship and final-year project – but with a promise of being infinitely more expressive and intuitive than the SAT solvers I worked with. At the time I joined the project the community was porting Lean 3 to Lean 4, and they were pleading for volunteers to port thousands of files of mathematical theories formalised in Lean 3 – so I jumped right in.
Soon enough I couldn't stop. Not only was I reserving entire trees of files to port and working much faster than other volunteers, I was learning the language at a far deeper level than could be achieved had I gone through textbook-style resources like the Natural Number Game. Then I got my own ideas of new theories to formalise directly in Lean 4, such as Turán's theorem and Abel's limit theorem.
The port to Lean 4 officially ended on 16 July 2023, and I spent the next year doing low-level stuff in Lean. That ennui ended when the Carleson project was started to formalise one of the hardest proofs in mathematics. Its tasks were very appealing to me, not requiring many new definitions and proofs to be hammered out, but rather a long string of bound computations involving basic measure theory and combinatorics. I ended up formalising a great deal of tasks there (up to and including the time of this journal).
Around the same time I was interested in contract bridge and riichi mahjong, and would sometimes use my SMRT staff pass (doubling as a free travel pass on all Singaporean public transport) to go to NUS for student-run game nights for those two games. On one such occasion I met another undergraduate and learned that he lived very near my own house, and when I told him about my prior studies he asked me if I was going to return for Masters or PhD.
At that point I was seized by the realisation that my Lean experience was my ticket back to university. I began frantically searching NUS's computer science professors and my former lecturers for referrals, eventually settling on Ilya Sergey as my preferred PhD advisor (it is possible to skip masters and go directly to PhD, as happened here). I started my application for PhD in October 2024 and submitted it about a week before the deadline in early November 2024.
Through the new year and into February 2025 I began being contacted by AI companies using Lean, offering me contractor work while I was waiting for my application results. I applied for and was accepted into two such positions (though I soon forgot about one of them because they weren't holding me to anything and were paying significantly less than the other company). And then, on 25 April 2025, I got the massive news – my PhD application had been accepted and I would start on 4 August 2025.
That would of course require me to resign from SMRT, and I have done that. Considering everything, though, SMRT supported me well throughout these three years, providing me with some train-related coding problems yet leaving enough free time to pursue the interests that, in a merry and colourful way, led to me landing the PhD programme. For this I shall always be grateful, and I look forward to a future where I can really put my knowledge at the service of the world.
Jeremy Tan / Parcly Taxel
Duskie
~greycait
Ooooo Congrats! :) This is amazing news!
