Chinese tactics

Stream: lean4

[Kevin Buzzard]

I am being visited by a Chinese number theorist today (an old friend) and they want to ask me about setting up a Lean course in the maths department at PKU. Am I right in thinking that it would basically be a triviality to translate tactics' names into Chinese by just defining a new tactic (whose name has Chinese characters) and defining it to be equal to the corresponding English-named tactic? I know Patrick did much more than this with French, I guess I'm just checking that there should be no issues with unicode characters in tactic names which could cause problems down the line. I don't know what they're going to ask me about but I imagine that this might come up.

[Mario Carneiro]

There is one complication, which is that lean's identifier class is not unicode-safe, it includes latin and greek and some kinds of mathematical text but much less than the unicode XID_Start / XID_Continue classes. For keywords (like tactics) this is fine, but it means that you won't be able to write let 点 := (1, 2)

[Mario Carneiro]

you can still write such identifiers with let «点» := (1, 2) but this is pretty annoying

[Yufei Liu]

i personally think the lean tactics no need to be translated into Chinese, as most (99.9999%) of coding in China are in English, PKU is one of the finest institution in China so i think you can assume students there are very familiar with English coding. Maybe a course in LEAN only means the teaching language can be Chinese.

[Yufei Liu]

I don't know what they're going to ask me about but I imagine that this might come up.

I seriously doubt that

Take your natural number game for an example, perhaps translating the explanation part to Chinese is enough, no need to translate the tactics and theorems, the language itself

[Kevin Buzzard]

Thank you for these comments Yufei! I was just conjecturing what my friend would ask me and it sounds like I was wrong here.

[hahalol]

Kevin Buzzard said:

Thank you for these comments Yufei! I was just conjecturing what my friend would ask me and it sounds like I was wrong here.

Hi Kevin B have you given up on always being two steps ahead of trends in Popularizing Proof Assistants? Of anyone else you should not fall into the flawed argument above, and instead do a small investment with a huge potential social-impact and 10x return payoff.

https://1337777.github.io/

is already a prototype Chinese Coq (鸡算计) where commands names, keywords names, tactics names, etcs.. are all translated, together with a tutorial introduction/documentation to Coq explained in Chinese too! This is the ultimate popularization of proof assistants, whose target demographic could now include (millions of) highschool students too!

It would not be hard to do the same for lean4, would you be happy to invest support in such academic research? Thank you for your attention to this matter.

[Mauricio Collares]

(deleted)

[Bulhwi Cha]

hahalol said:

https://1337777.github.io/

Oh, there's also Korean Coq (수탉수학, "Rooster Math") here. I want to know how to translate Lean code into Korean.

[Mario Carneiro]

@hahalol Note: contrary to popular opinion, Kevin B is not the leader of lean, and does not set the priorities for the project.

[Mario Carneiro]

The lean language is quite capable of being flexible enough to translate all the keywords, although translating the theorems in the core library and mathlib is rather more difficult, and as mentioned while you can have your own theorems named in any language, you will have to use «» around the identifiers if they are not in latin-ish script. I think this could be fixed (in core) with an RFC if desired though.

However, we would still need a maintainer for each supported language, likely supplied by a project that defines all the tactics and syntax. Perhaps someone here would like to volunteer to maintain them?

[Bulhwi Cha]

I'd love to volunteer, but I'm not sure if I'm capable of maintaining Korean translations of all the Lean keywords.

[Arthur Paulino]

EDIT: nvm, it's about adapting/maintaining tactics syntax

[Mario Carneiro]

It's possible we could set up a meta-translation framework, so that we only need to have keyword translations and automatically copy the syntax declarations from lean. That would help avoid divergence since presumably the syntax of tactics will change much more frequently than the set of words that need translation

[Arthur Paulino]

I think the meta-translation path is also more reusable like for instance if someone wants to support a translation to more languages

[Mac Malone]

My library Partax provides a meta-translation of syntax to parsers (Sorry for the shameless self-plug). One could probably use a similar approach (or even configure Partax) to translate between syntaxes.

[Kevin Buzzard]

I talked to Liang today and he didn't seem remotely interested in translating any lean code into Chinese :-)

[Utensil Song]

Kids in China are either already exposed to years of English education before learning programming (for the less young generations), or exposed to scratch-style programming environments in kindergarten/primary school with Chinese characters on the building blocks (for the younger generations). There's never a need for writing Chinese during programming, according to such cognitive pathways.

Although, this is a fun idea, so there are two famous attempts:

1. the old (since 2003) attempt is known as Yi language (Yi means both easy and changing as in the ancient Book of Changes ), which is mostly writing C-like language but keywords and core function names in Chinese.

Most have heard of it, but it's never adopted widely. The language design and the ecosystem is completely obsolete nowadays. The English style word order and the translation tone of Chinese keywords make it very unnatural to write, and even more difficult to remember how to write correctly, compared to just few frequently used English keywords in most programming languages.

2. the new (since 2019) attempt is wenyan-lang, while the technical aspect of it is relatively modern (like compiling to JS/Python, having a package manager and a small but good ecosystem etc.), the language it uses is ancient Chinese(both ancient words and ancient grammar), which is a mandatory part in the education throughout primary school to high school, so people are familiar with it and like it.

Also, designing such a language is strongly motivated by reproducing (the writing style of) algebraic solutions in ancient Chinese mathematical books, which are mentioned in textbooks, so people in China are proud of these books. The reproduced results are collected in its online editor here (maybe-slogan: write ancient Chinese, do math).

[Utensil Song]

An example of the program in wenyan-lang (typeset in ancient Chinese style, reads from top to bottom, then right to left) that prints a mandelbrot:
image.png
The author creates more of these programs and gathers them into a book, also available as downloadable PDFs: https://github.com/wenyan-lang/book/releases

[Schrodinger ZHU Yifan]

Well, I am personally not a fan of programming in Chinese. While some particular Chinese PLs look nice, I myself find it annoying typing Chinese when doing programming — even with intelligent IME, (in most cases) it might still acquires extra key strokes to type out a word in Chinese than a word of the same meaning in English.

Tactics mode, when compared with program mode, tries hard to reduce steps so that you can write a proof as fast as possible. (Of cuz, clearance is also a consideration). Thus, I prefer keeping it in an input-friendly way.

However, a friendly and well-written guide in Chinese introducing Lean will definitely be useful to make it popular.