Seoul, South Korea

Stream: Geographic locality

[Juneyoung Lee]

Hi all, here is Seoul / Korea

[Shim SeongWoo]

Hello, Juneyoung! this is Seongwoo.
We've been working for translate Natural Number Game in Korean as Semmalgil team last 3 month.
when you have some time visit and see our github team project

https://github.com/semmalgil/natural-number-game-kr

[Kevin Buzzard]

Hey just to be clear -- feel free to advertise and distribute the translation, you certainly have my blessing

[Minju Kim]

Hi, I'm Minju Kim also from Semmalgil team.
The goal of our team is contributing to Korean education of math using Lean programming language.
We think Lean makes us easier for learning logical base for math and also verifying our mathematical knowledge.
So we're translating Natural Number Game for our first small project.
Having lots of things to do for making effective and easier education contents, we would need much help from this community. Thanks in advance!

[Patrick Massot]

Great! Did you use the translation setup that I prepared a couple of years ago (when I hoped some people would volunteer to translate to French) or did you do it by editing the Lean files?

[Minju Kim]

We're using your setup, If I'm right. We created a file 'locale/kr/LC_MESSAGES/content.po' and we are adding translation to the file using program 'omegaT'.
For now, we are studying Lean, and don't know enough for editing Lean files. Using content.po file is convenient, I think.

[Patrick Massot]

Yes, this is my setup. This makes me very happy!

[Andrés Goens]

@Patrick Massot is there a stream/thread where you discuss this setup? I could only find this thread about (language) localization that didn't go anywhere. I'd be willing to give this a try and translate some stuff to Spanish using this setup as well!

[Patrick Massot]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Natural.20number.20game.20translation

[sedev627]

Is there any korean translation of lean tutorial?

[sedev627]

I've been translating since yesterday when I started learning Lean.
Just now, 00_first_proofs.lean translation was completed.

[Bulhwi Cha]

Not yet. Instead, I was thinking of translating Theorem Proving in Lean 4 into Korean.

[sedev627]

Bulhwi Cha said:

Not yet. Instead, I was thinking of translating Theorem Proving in Lean 4 into Korean.

Is it completed? or Did it stop?

[Bulhwi Cha]

@Shim SeongWoo already translated the first two chapters, and I'm going to review them next month.

[Shim SeongWoo]

I recently translated up to chapter 3.
Here is my github project.

https://github.com/shimsw20/Theorem-Proving-in-Lean-4_kr

I'm just translating the original html file into Korean using omega T.
I'm also solving Practice problem of chapter 3 now.

[Jineon Baek]

Decided to drop my name here. I'm Jineon Baek, a fourth-year UMich PhD student. I use Lean mainly to formalize mathematical theorems, both my own and existing ones. But I also have a little bit of exposure to PL as well and also interested in functional programming and verification of softwares as well. Here are some works that I've done (second one is done with @Seewoo Lee:

https://github.com/jcpaik/erdos-tuza-valtr
https://github.com/seewoo5/lean-poly-abc

I'd love to talk about both the use of Lean in pure math and software formalization. Feel free to DM me if you are interested!