Karl Palmskog (Jan 05 2021 at 21:23): 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.)
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
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
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!
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?
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/
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
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...
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
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
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
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".
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.
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.
Karl Palmskog (Jan 06 2021 at 11:21):oh, so it's that guy... now I connected the dots.
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.
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.
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...
Li-yao (Jan 15 2021 at 00:01):"Jisuanji" is a very nice translation of Coq :D
Yao Li (Jan 15 2021 at 01:43):LOL indeed!
Karl Palmskog (Jan 15 2021 at 02:59):wow, so the Chinese is actually about Coq and not about something random. thanks!
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.
Shenghao Yuan (Jan 15 2021 at 12:28):Li-yao said:
"Jisuanji" is a very nice translation of Coq :D
cock computation machine?
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...
Paolo Giarrusso (Jan 15 2021 at 19:47):"the video is evil"? oh dear
Paolo Giarrusso (Jan 15 2021 at 19:47):nothing wrong with translating Coq tactics to another language, IMHO
Paolo Giarrusso (Jan 15 2021 at 19:48):other posts in English by OOO1337777 raise more questions
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).
Paolo Giarrusso (Jan 15 2021 at 23:26):I was trying to be nice, but fair.
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
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: Apr 18 2024 at 09:02 UTC