Zulip Chat Archive

Stream: Geographic locality

Topic: Seoul, South Korea


Juneyoung Lee (Apr 12 2020 at 15:56):

Hi all, here is Seoul / Korea

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

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

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!

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?

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.

Patrick Massot (Feb 13 2022 at 09:51):

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

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!

Patrick Massot (Feb 14 2022 at 12:23):

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

sedev627 (Feb 15 2022 at 13:58):

Is there any korean translation of lean tutorial?

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.

Bulhwi Cha (Feb 15 2022 at 14:07):

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

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?

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.

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.

Jineon Baek (Apr 09 2023 at 22:44):

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!


Last updated: Dec 20 2023 at 11:08 UTC