learning about lean alone in south korea

Stream: general

[Bulhwi Cha]

It's been almost a year since I started learning about Lean while looking into Metamath, Linux administration, Git, and Web development. I've been able to do these because I took a leave of absence from Korea Aerospace University in the summer of 2020; it was challenging to spend time learning about things that aren't directly related to aerospace engineering when I was in university.

On the other hand, each of my friends and other people stopped learning about Lean for one or more of the following reasons: it turned out they weren't interested in formal mathematics or functional programming; they had difficulty reading online textbooks and documents written in English; or they became busy with their work or research.

I think it's safe to say that in South Korea, you can't find a professor in mathematics who uses a proof assistant to teach themselves and students how to formalize mathematics. This situation leads to a lack of students who wish to study formal mathematics; they aren't interested in it or don't have time to research it.

As I said in my introduction, I aim to develop games for mathematics education and study symplectic geometry so I can formalize them. Ironically, it looks like I'd be better off using Lean and Metamath Zero to achieve my goals if I dropped out of university. Thus I decided to leave the university this summer. I hope future generations of students in my country won't have obstacles to formalization of mathematics using proof assistants.

[Kevin Buzzard]

@Hyunsik Chae came to my undergraduate workshop -- he's another Korean lean user.

[Bulhwi Cha]

We met each other online last September. But we haven't talked much because he's been busy finishing his Bachelor's thesis and preparing for graduate school.

[Hyunsik Chae]

Hello and happy new year! Bulwhi has been in touch with me for a couple of months but I was too busy for close connection due to my graduation.
By the way, I would love to share that some professors in Korea have recently started to use Lean (unofficially). If you want to know more please let me know :)

[Bulhwi Cha]

Do they know about this Zulip chat? If they don't, could you tell them about it?

[Bulhwi Cha]

Hyunsik Chae said:

By the way, I would love to share that some professors in Korea have recently started to use Lean (unofficially). If you want to know more please let me know :smile:

If we don't know when they'll use Lean "officially," students in KR won't have the chance to formalize mathematics with a tutor's guidance anytime soon.

[Hyunsik Chae]

Quite frankly I doubt it will happen in 1-2 years.

[Jineon Baek]

Hi! A Korean grad student at UMich majoring in math here. I've been using Lean for a couple months as well. I also had to study it by myself and it was tough for me. For me starting on a project and formalizing what I want to, and asking newbie things on Zulip and Xena discord channel has helped a lot. I think building a new culture of math takes quite a bit of time, but otoh I think this also puts us in a position where we could plant the culture in Korea if given a chance. I am by no means an expert, but feel free to hit me up if you are interested in having a chat.

[loki der quaeler]

it's likely everyone reads this channel, but in case not, there is #Geographic locality for this sort of specific thing that you might want to post in as well.