teaching lean alone in south korea

Stream: Lean for teaching

[Bulhwi Cha]

On January 21, 2023, I wrote a message titled "Learning about Lean alone in South Korea" in the Lean Zulip chat. At the moment, I know of three Korean graduate students who have used Lean to formalize mathematical theories. However, I still haven't heard of a professor of mathematics or computer science who lives in South Korea and uses Lean to work on formalization of mathematics or software and hardware verification. As a result, most Korean students don't have the opportunity to learn about it at universities or other institutions.

Luckily, I was selected as a mentor for one of this year's hands-on training programs (Korean) at the Open-Source Software Contribution Academy (OSSCA), organized by NIPA's OSS Support Center (Open UP). Since September 9, I've been using "Theorem Proving in Lean 4" to teach Lean to my twelve mentees, including software developers, undergraduates, graduates, and a high-school student. We'll also translate the Natural Number Game into Korean starting this week. The mentorship program will end on October 25.

I'm also making a video series (Korean) where I read the textbook and explain its key points in Korean. I didn't expect to take about eight hours to cover Chapter 2, Dependent Type Theory. I'm trying to explain everything my mentees are unfamiliar with because most of them are new to propositional and first-order logic, let alone type theory. So, I'm not sure if I'll be able to finish the book before my mentoring ends. I'm okay with my progress; my mentees already look busy learning Lean's type theory while doing their main jobs.

Lastly, each of us will create a git repository containing solutions to some of the exercises in "Theorem Proving in Lean 4." Mine is tpil-solutions. It doesn't have any solutions yet, but you can check out the quiz I made for Chapter 2. I hope my videos and learning materials will help more Koreans get to know proof assistants like Lean and understand how to use them.