My PhD

Stream: general

[Jeremy Tan]

I have to thank the entire Lean community for this. It all started when I stumbled upon you people porting Lean 3 to Lean 4 in March 2023, then I got attracted to Carleson in 2024, and more recently I've been approached by multiple AI companies and accepted positions at them…

But this letter beats everything else.

image.png

I indicated @Ilya Sergey as my advisor when I applied, but this is not set in stone yet.

[Floris van Doorn]

Congratulations! It's well deserved, given how much hard work you've done for the port and the Carleson project.

[A.]

Congratulations! Do you really think that it's your engagement with the Lean community that has brought these opportunities? Are AI companies and universities counting Mathlib PRs?

[Jeremy Tan]

A. said:

Do you really think that it's your engagement with the Lean community that has brought these opportunities?

Through the Zulip I learned that @George Pîrlea was working in NUS, and that led me to my prospective advisor Ilya. So, at least in part, yes

[Jeremy Tan]

For the record, I announced some months earlier that I was applying for this PhD at #Carleson > Outstanding Tasks, V4 @ 💬

[Shreyas Srinivas]

Jeremy Tan said:

I have to thank the entire Lean community for this. It all started when I stumbled upon you people porting Lean 3 to Lean 4 in March 2023, then I got attracted to Carleson in 2024, and more recently I've been approached by multiple AI companies and accepted positions at them…

But this letter beats everything else.

image.png

I indicated Ilya Sergey as my advisor when I applied, but this is not set in stone yet.

Congratulations. I remember your absolutely gargantuan contribution to the port. This is well deserved.