Zulip Chat Archive

Stream: Geographic locality

Topic: Seoul, South Korea


view this post on Zulip Juneyoung Lee (Apr 12 2020 at 15:56):

Hi all, here is Seoul / Korea

view this post on Zulip Shim SeongWoo (Feb 13 2022 at 06:51):

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

view this post on Zulip Kevin Buzzard (Feb 13 2022 at 07:59):

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

view this post on Zulip Minju Kim (Feb 13 2022 at 09:16):

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!

view this post on Zulip Patrick Massot (Feb 13 2022 at 09:25):

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?

view this post on Zulip Minju Kim (Feb 13 2022 at 09:41):

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.

view this post on Zulip Patrick Massot (Feb 13 2022 at 09:51):

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

view this post on Zulip Andrés Goens (Feb 14 2022 at 11:22):

@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!

view this post on Zulip Patrick Massot (Feb 14 2022 at 12:23):

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

view this post on Zulip sedev627 (Feb 15 2022 at 13:58):

Is there any korean translation of lean tutorial?

view this post on Zulip sedev627 (Feb 15 2022 at 14:01):

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

view this post on Zulip Bulhwi Cha (Feb 15 2022 at 14:07):

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

view this post on Zulip sedev627 (Feb 15 2022 at 14:13):

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?

view this post on Zulip Bulhwi Cha (Feb 15 2022 at 14:47):

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

view this post on Zulip Shim SeongWoo (Feb 17 2022 at 12:58):

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.


Last updated: Oct 06 2022 at 06:24 UTC