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.)
I'm at least looking forward to more Twitch-like streaming of proof assistant use in general
The future is already there: weird videos in mandarin with Chinese influencers on Coq https://www.youtube.com/watch?v=odjd0En33ag
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!
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?
@Karl Palmskog originally found following https://www.reddit.com/r/dependent_types/comments/kit8yz/coq365_coq_math_proof_assistant_addin_inside/
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
High level of WTF if you ask me, but the author is famous for his outlandish posts on Coq-club so...
has he posted recently? I try to follow Coq-club now and then, but have never seen him
Not in recent times AFAIR, though he's still active as witnessed by the reddit posts
There are several github accounts that seem related to that person, as well as the youtube ones
I didn't want to say it (and we're certainly OT), but the favorite description was "crank".
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.
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.
oh, so it's that guy... now I connected the dots.
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.
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.
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...
"Jisuanji" is a very nice translation of Coq :D
LOL indeed!
wow, so the Chinese is actually about Coq and not about something random. thanks!
[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.
Li-yao said:
"Jisuanji" is a very nice translation of Coq :D
cock computation machine?
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...
"the video is evil"? oh dear
nothing wrong with translating Coq tactics to another language, IMHO
other posts in English by OOO1337777 raise more questions
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).
I was trying to be nice, but fair.
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
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: Jun 01 2023 at 11:01 UTC