Stream: Miscellaneous

Topic: Streaming proof assistant use


view this post on Zulip Karl Palmskog (Jan 05 2021 at 21:23):

maybe there will come a time when (organizations behind) proof assistants will fight for high-profile users by monetary means, like how streaming platforms fight for streamers (of games, etc.)

view this post on Zulip Karl Palmskog (Jan 05 2021 at 21:28):

I'm at least looking forward to more Twitch-like streaming of proof assistant use in general

view this post on Zulip Pierre-Marie Pédrot (Jan 05 2021 at 22:38):

The future is already there: weird videos in mandarin with Chinese influencers on Coq https://www.youtube.com/watch?v=odjd0En33ag

view this post on Zulip Paolo Giarrusso (Jan 05 2021 at 22:51):

The #coq channel in IRC has long been confused about #OOO1337777, but I hadn't seen that nick in a long time. And never seen the author!

view this post on Zulip Karl Palmskog (Jan 05 2021 at 23:09):

what the heck? That's some weird stuff going on. Perhaps someone who knows Mandarin can summarize what she's saying? Is it in any way related to Coq?

view this post on Zulip Pierre-Marie Pédrot (Jan 05 2021 at 23:14):

@Karl Palmskog originally found following https://www.reddit.com/r/dependent_types/comments/kit8yz/coq365_coq_math_proof_assistant_addin_inside/

view this post on Zulip Pierre-Marie Pédrot (Jan 05 2021 at 23:15):

There are a handful of other weird videos by OOO1337777 if you start looking from the suggestions, including weird reading of topos theory in French by a Cameroonese woman

view this post on Zulip Pierre-Marie Pédrot (Jan 05 2021 at 23:16):

High level of WTF if you ask me, but the author is famous for his outlandish posts on Coq-club so...

view this post on Zulip Karl Palmskog (Jan 05 2021 at 23:17):

has he posted recently? I try to follow Coq-club now and then, but have never seen him

view this post on Zulip Pierre-Marie Pédrot (Jan 05 2021 at 23:18):

Not in recent times AFAIR, though he's still active as witnessed by the reddit posts

view this post on Zulip Pierre-Marie Pédrot (Jan 05 2021 at 23:18):

There are several github accounts that seem related to that person, as well as the youtube ones

view this post on Zulip Paolo Giarrusso (Jan 06 2021 at 00:10):

I didn't want to say it (and we're certainly OT), but the favorite description was "crank".

view this post on Zulip Paolo Giarrusso (Jan 06 2021 at 00:14):

even if it's hard to be sure, and there might be some technically impressive components. It's probably a pity, but I'm not sure we've ever witnessed bidirectional communication with them.

view this post on Zulip Guillaume Melquiond (Jan 06 2021 at 08:46):

Karl Palmskog said:

has he posted recently? I try to follow Coq-club now and then, but have never seen him

Last time was on Nov 3.

view this post on Zulip Karl Palmskog (Jan 06 2021 at 11:21):

oh, so it's that guy... now I connected the dots.

view this post on Zulip Yao Li (Jan 14 2021 at 22:50):

Karl Palmskog said:

what the heck? That's some weird stuff going on. Perhaps someone who knows Mandarin can summarize what she's saying? Is it in any way related to Coq?

She says she has translated the Coq terms from English to Chinese. The Emacs window shows a Coq file but with all the keywords such as Definition, Proof, refine (this one got translated incorrectly), etc. in Chinese.

view this post on Zulip Yao Li (Jan 14 2021 at 23:02):

In the beginning of the video, she says she was admitted by some school (seems to be the AnthropLOGIC school from the title), and she chose to translate Coq from English to Chinese (supposedly as a school project?). Then this was followed by a very brief introduction of Coq (that it is a theorem prover) (so it is indeed related to Coq). In the end she also mentions the translation does not break the correctness of Coq.

view this post on Zulip Yao Li (Jan 14 2021 at 23:06):

I'm still very confused of what is going on even though I can understand what she says... The video also contains some broken Chinese on the screen that I do not understand starting from 10 secs...

view this post on Zulip Li-yao (Jan 15 2021 at 00:01):

"Jisuanji" is a very nice translation of Coq :D

view this post on Zulip Yao Li (Jan 15 2021 at 01:43):

LOL indeed!

view this post on Zulip Karl Palmskog (Jan 15 2021 at 02:59):

wow, so the Chinese is actually about Coq and not about something random. thanks!

view this post on Zulip Zheyu Shen (Jan 15 2021 at 12:01):

[Quoting…]
So what's the whole story? It feels as if he's yet another person who turned delusional like the late Terry Davis. The TempleOS guy.

view this post on Zulip Shenghao Yuan (Jan 15 2021 at 12:28):

Li-yao said:

"Jisuanji" is a very nice translation of Coq :D

cock computation machine?

view this post on Zulip Shenghao Yuan (Jan 15 2021 at 12:43):

Pierre-Marie Pédrot said:

The future is already there: weird videos in mandarin with Chinese influencers on Coq https://www.youtube.com/watch?v=odjd0En33ag

The streamer is from a professional team: the team is not professional to Coq, but professional to streaming!!!

Her work (Maybe someone from her team) is so weird: just translating the English tactics into the Chinese version.
So when you do prove, you just need to write the Chinese one, of course it will never break the correctness of Coq.

I send the link to one Chinese Coq community (about 200 people), They commented that the video is evil...

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 19:47):

"the video is evil"? oh dear

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 19:47):

nothing wrong with translating Coq tactics to another language, IMHO

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 19:48):

other posts in English by OOO1337777 raise more questions

view this post on Zulip Shenghao Yuan (Jan 15 2021 at 20:31):

Paolo Giarrusso said:

nothing wrong with translating Coq tactics to another language, IMHO

this behavior is useless. I guess most Chinese coq users don't a Chinese tactic, because it seems so stupid:

when you do code,you need two language (English one and Chinese one);

if you don't know how to use a tactic, you need to, firstly translate it into the english one, and search the coq user guide...

The streamer just renamed the coq tactics, she didn't define a new tactic, or make the proof more concise and simple.

What's more, it is harmful for a beginner: it hides the original meaning because of the terrible transformation. For instance, She translates therefine into jia xi(qiujing or xihua is the correct version).

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:26):

I was trying to be nice, but fair.

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:28):

Ignoring this translation, I think it can be a tricky question — I'm sure many would object to my actual recommendation (to do CS, get fluent in written English), and they'd object more if I were a native English speaker instead of an Italian

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 23:30):

but that discussion belongs elsewhere. I'm confident there's not enough documentation for Coq in Italian but I'll stick to that.


Last updated: Aug 14 2022 at 12:03 UTC