Poznań, PL

Stream: Geographic locality

[Miriam Kosik]

Hi, I am a Physics PhD graduate living in Poznań, Poland. I have just found out about the existence of Lean and other theorem provers yesterday and I am really excited about the topic. I have a strong background in programming (currently working in ML for a medical applications) but I miss more scientific, "low-level" work and I love mathematics. I love to tackle problems at a deep basic level. I taught calculus on various levels during my PhD and enjoyed it a lot.

It seems that there are not many people from my country here but maybe someday... It would be really amazing to create an on-site-meeting group. For now, luckily there is Internet.

[Filippo A. E. Nuccio]

Hi @Miriam Kosik , welcome! I have seen you enrolled in our Lean in Lyon workshop in a month time, or so, and I hope you will find it interesting. In the meantime, you will find a lot of nice and helpful people around. Have you tried playing with the NNG?

[Miriam Kosik]

Filippo A. E. Nuccio said:

Hi Miriam Kosik , welcome! I have seen you enrolled in our Lean in Lyon workshop in a month time, or so, and I hope you will find it interesting. In the meantime, you will find a lot of nice and helpful people around. Have you tried playing with the NNG?

Thanks, I am looking forward to it. I have already found lots of interesting material here and on the leanprover community. I am amazed how much has been done already. I installed Lean 4 yesterday and I am currently working through "Theorem Proving in Lean 4" but I will surely try to play the game as well.

[Filippo A. E. Nuccio]

FYI: Although Lean 4 has been out for a while and one can surely start using it, it might be relevant to know that mathlib, the huge math library you are probably referring to, is still written in Lean 3. There is a definitive plan to port everything to Lean 4, but for the time being most of the community is still working on Lean 3.