Good afternoon!
I’d like to tell you about a major case of violation by the person with the nickname @5HT.
He hired me for type theory research and I worked successfully from 2018 to 2022 until February 28 he decided to break any relationship with me and kicked me out of the Groupoid organization where my projects were located.
A few days later, all my commits in that organization were no longer connected to my account.
@5HT said that this caused by ban in organization, but, very strangely, @forked-from-1kasper disappeared in contributors statistics (commits are still available, so it’s easily to check existence of my commits) in:
- https://github.com/groupoid/anders/graphs/contributors
- https://github.com/groupoid/homotopy.dev/graphs/contributors
- https://github.com/groupoid/ivy.mike/graphs/contributors,
but not in
- https://github.com/groupoid/principia/graphs/contributors
- https://github.com/groupoid/ground.zero/graphs/contributors
- https://github.com/groupoid/castle.bravo/graphs/contributors
- https://github.com/groupoid/hurricane/graphs/contributors
- https://github.com/groupoid/smiling.buddha/graphs/contributors
- https://github.com/groupoid/canopus/graphs/contributors.
After that, he twitted in his account @infinitystack:
https://twitter.com/infinitystack/status/1499341999039782913
(translation below, archived version)
that I’m not now considered as one of Anders author, but rather as his russian slave, because
- this work was paid
- @5HT has more commits in this repository
(And this is an easily verifiable manipulation, because his commits are mainly about library, *.anders files, of language, but not about language itself, i.e. *.ml files).
And recently, he removed me from LICENSE file without asking, which is an obvious violation of the license.
April 6 Update. Commit history from https://github.com/groupoid/anders/commits/main was removed. You may compare this repository with https://github.com/forked-from-1kasper/anders.
April 7 Update. He removed me from OPAM configuration file too: https://github.com/groupoid/anders/commit/024099a150aaff11b9f4c50748f9239d9141fb71.
Moreover, he deleted all authors of groupoid/CCHM (known earlier as groupoid/cubical).
April 8 Update. Commit history from https://github.com/groupoid/groupoid.space, https://github.com/groupoid/cubical.systems and (important) https://github.com/groupoid/CCHM was deleted.
June 17 Update. License in all projects from https://github.com/o89 was changed to his very strange non-free DHARMA license. It is very funny, because nothing in this repository works with new versions of Lean 4 (since transition to bundled LLVM/clang or maybe earlier).
Also look here, here, and here for more interesting comments from @5HT.
July 16 Update. Something strange happened: stars in groupoid/anders disappeared (last time I saw 82 stars there, but in archive there is only page with 84 stars from the 6th of June; two stars disappeared later). The same thing happened with forks, so it’s not very hard to find that they are now here. Such things usually happens when main repository was deleted: all forks become fork of some other fork of the deleted repository; but this could not happen now, because 1) redirect from forked-from-1kasper/tt (this is where groupoid/anders was created) is still alive, 2) there is still badge in my profile confirming that I created groupoid/anders, 3) there is nothing about that in Gitter (although I’m not sure that something should be in Gitter), 4) https://github.com/groupoid says that groupoid/anders was modified 21 days ago (if repository was recreated, there should be some other date). Maybe this could happen if repository was hidden and then opened from public, but I’m not sure about this too. It’s funny that @5HT in his profile unpinned groupoid/anders after this (it’s not very hard to verify that groupoid/anders was here earlier). This says a lot about what he is actually worried about.
In addition, https://anders.groupoid.space/ doesn’t work now. I don’t know how long it’s broken and whether it’s related to stars.
July 23 Update. https://anders.groupoid.space/ works again.
I did a little investigating, and found that this is not the first time that other people’s authorship has been erased by @5HT.
If you look at the code of the smiling.buddha project, you will quickly notice that a considerable part of this library is just a rearrangement (with some name changes and added comments) of the cubicaltt typechecker library examples, for example:
s1.ctt in cubicaltt library and circle.ctt in smiling.buddha
helix.ctt in cubicaltt library and helix.ctt in smiling.buddha
univ.ctt in cubicaltt library and univalence.ctt in smiling.buddha
This library contained some original code and I was curious to find out where it came from. (And it was pretty difficult.)
Originally there was a project called EXE, which @5HT hired several people to develop.
If we go to the repository of this project now, we find the only author is @5HT. Fortunately for us, there are many forks of this project left by which other authors can be identified.
https://github.com/silky/exe/graphs/contributors
The real, working code was written by zraffer, who was later erased from the authors, while @5HT mostly did a lot of trivia commits, giving comments and correcting typos.
Looking through the EXE forks, you will notice repositories named infinity share a common history. The list of infinity contributors includes a person with nickname nponnecop who, I know for a fact (full logs), wrote this code for money and whose major contribution has also been erased from history.
April 11 Update https://gist.github.com/forked-from-1kasper/06d241303cc314b35c291c38e61a5e0c?permalink_comment_id=4128741#gistcomment-4128741
There is a long list of repositories, with the loss of commit history and, the most important, authorship.
For example: in groupoid/pure, you can see from the commits how the authors of the project disappeared: Andy Melnikov, Paul Lyutko.
April 5 Update. https://github.com/groupoid/pure (or OM, or PTS) was renamed to Henk and recreacted as https://github.com/groupoid/henk/ without saving history; original repository moved to https://github.com/5HT/henk. After around a day history from https://github.com/5HT/henk was erased too (probably through delete + new), and history from https://github.com/groupoid/henk/ was erased again (i.e. a second time a day).
https://github.com/groupoid/homotopy was deleted, but you still can check and compare latest saved version with earlier forks listed below.
Other project, called homotopy (or HTS, or EXE), have 8 contributors, but there is only one, in credits section of README.md, and in commit history.
His favorite strategy is to change the names of the projects several times, merge and split the code again to make it harder to suspect him of stealing, so it is quite difficult to recognize the connection between his repositories.
I’m still investigating, and apparently this person’s entire career is based on hiring people and then appropriating their work, and in some cases directly stealing code from other projects without attribution.
In my opinion, the Github community shouldn’t tolerate people like @5HT.
Best wishes and hope for proceedings with this person.
Translation:
P.S. I also attach a (probably incomplete) list of forks of these repositories:
https://github.com/forked-from-1kasper/henk
https://github.com/forked-from-1kasper/homotopy
https://github.com/forked-from-1kasper/homotopy.dev
https://github.com/5HT/5HT
https://github.com/AlexZolcman/CCHM
https://github.com/5HT/tonpa.guru
https://github.com/adept/infinity
https://github.com/diasbruno/pts
https://github.com/DmytroMitin/infinity
https://github.com/e42s/exe
https://github.com/e42s/infinity
https://github.com/e42s/om
https://github.com/erlang-cn/hts
https://github.com/erlang-cn/pts
https://github.com/hardentoo/infinity
https://github.com/ilya-klyuchnikov/pure
https://github.com/jfrancese/cubical
https://github.com/k-haze-nil/om
https://github.com/knurdDongle/infinity
https://github.com/m-2k/exe
https://github.com/m-2k/om
https://github.com/mafm/pure
https://github.com/nau/om
https://github.com/nponeccop/hts
https://github.com/nponeccop/infinity
https://github.com/nponeccop/n2o.hs
https://github.com/nponeccop/om
https://github.com/py361/agda
https://github.com/pyzh/cubical
https://github.com/pyzh/infinity
https://github.com/pyzh/om
https://github.com/Randl/om
https://github.com/sam-mix/pts
https://github.com/silky/exe
https://github.com/spivakov/om
https://github.com/ulidtko/exe
https://github.com/xafizoff/agda
https://github.com/xafizoff/cubical
https://github.com/xafizoff/hcomp
https://github.com/xafizoff/om
https://github.com/yurrriq/exe
https://github.com/yurrriq/om
https://github.com/Zabrane/pure
https://github.com/zeitraffer/om
https://github.com/zaoqi-unsafe/exe
April 5 Update. List of renames and transfers:
https://github.com/groupoid/pure → https://github.com/5HT/henk + https://github.com/groupoid/henk
https://github.com/groupoid/homotopy deleted completely
https://github.com/groupoid/smiling.buddha → https://github.com/groupoid/CCHM
https://github.com/groupoid/principia → https://github.com/groupoid/bertrand
https://github.com/groupoid/castle.bravo → https://github.com/5HT/nicolas
https://github.com/groupoid/hurricane → https://github.com/groupoid/valery
https://github.com/groupoid/ivy.mike → https://github.com/5HT/ivy.mike
https://github.com/groupoid/canopus → https://github.com/5HT/canopus
April 6.
https://github.com/groupoid/ground.zero → https://github.com/5HT/ground.zero
https://github.com/groupoid/minitt → https://github.com/5HT/minitt
April 8.
https://github.com/5HT/hts-archive deleted
https://github.com/5HT/nicolas deleted (see https://github.com/forked-from-1kasper/bravo)
https://github.com/5HT/ivy.mike deleted (see https://github.com/forked-from-1kasper/ivy.mike)
https://github.com/5HT/canopus deleted (see https://github.com/forked-from-1kasper/canopus)
https://github.com/5HT/ground.zero deleted (see https://github.com/forked-from-1kasper/ground_zero)
https://github.com/groupoid/homotopy.dev deleted
https://github.com/groupoid/ant → https://github.com/5HT/ant
https://github.com/5HT/henk → https://github.com/groupoid/henk
April 14.
https://github.com/groupoid/bertrand → https://github.com/5HT/bertrand
https://github.com/groupoid/valery → https://github.com/5HT/valery
June 17.
https://github.com/5HT/bertrand deleted (see https://github.com/forked-from-1kasper/principia)
https://github.com/5HT/valery deleted (see https://github.com/forked-from-1kasper/hurricane)
https://github.com/5HT/minitt deleted
You're young fascist and you can't change the fact that you were sponsoring and supporting the war. I will tell all the truth about you, how you behaved in #CHLOR chats. About KHOHOLS and N-words you used, about humiliation and jokes about LGBTQ+ community.
No one was ever hired to develop EXE or HTS languages, this is fake. I paid little money to @zraffer for support and that's it. I added you to license and I removed. These are my projects, I can freely change this as I want. More than half of this information is fake russian propaganda and spreading misinformation about me which he replicates all over the Internet, trying to steal my accounts, unsuccessfully. You can ask directly to @zraffer and @nponeccop what code they wrote and where it is placed in repository.
Disgusting that I need to explain in public because of some young ruscist, while we have a full scale war. You have all history records, fork, rewrite everything, put your license and live with that in your fascist russia. How you can tell me what to do with my repositories? Insane russian imperialism!
All my works at @github from now on are licenced under the term of DHARMA LICENSE: https://5ht.co/license/
This is not ISC, this is new license. Please respect that!
Once this young fascist was my student, I taught him Modal HoTT after visiting Geometry in Modal HoTT workshop:
https://tonpa.guru/stream/2019/2019-03-16%20Geometry%20in%20Modal%20HoTT.htm
Now he is saying that everything he made was made by him alone, very funny. Not that it matters, I don't give a fuck, just small notice. I literally spend the same amount of time, and even have more commits in his fork than him and this is only in OCaml repo, disregarding HOMOTOPY.DEV homotopy library site and files homepages! You can compare this amount of work with your favourite redtt or Arend sites.
"This library contained some original code and I was curious to find out where it came from." Did you manage to investigate where my code came from? You calling me liar but there is no evidence EXE code was written by anyone execpt me, full history 848 commits. As I said you can ask directly to @zraffer and @nponeccop about their contribution. @zraffer was working mainly on poset and setoid encodings which were later completly removed from OM repository as non-finished. @nponeccop was paid only several times for N2O.HS port which was later substituted by work of @xafizoff @o3/n2o. But that was not even donation, Andy is a rich person, that was my declaration of intention to make something together. That is the truth. You are the person who is spreading misinformation about me for 44 days starting from day 1 of our Great Patriotic War. I'm still fighting in twitter with trolls from your #CHLOR channel. That is you who called us KHOHOLS on our HOMOTOPY.DEV channel publicly, and just after that incident you were immediately banned for CoC violation and for recognized fascist support at your #CHLOR channel. That is the truth. I already told you all of that. Your contribution will be completely swiped out.
I don't even know if this person is real or some FSS account that was implanted to @groupoid to hijack Ukrainian mathematical community. Pity that @github still not baning russian accounts, that are thretening Ukrainians, but providing a platform for further spreading of misinformation.
I just want you all to know that I'm 40 and I already finished my academical track record. I'm retired, I'm a teacher of Tibetan Buddhism, I have officialy registered religious organization @longchenpa here in Ukraine. He is maybe thinking that I'm like him 19 y.o. who want to have text battles in Internet. This is not true, you can see my public life in all social networks.
https://www.instagram.com/5ht/
https://www.facebook.com/namdak.tonpa/
https://twitter.com/tonpaguru
https://5ht.co/
The academia for me always was a hobby and sport for thinking, managing around 100 github repositories is not an easy task. I have in average 1500-5000 commits per year for last 10 years continuously, which means I can easily get TOP-10 Github contributors in any state around the world, including China, California (USA) and Russia.
In next life I don't want to be born like famous mathematician, I want to be born like regular Ukrainian. Now I'm just trying to protect my students from these barbarian people.
A person who lives only with thoughts about mathematics, without a spouse, pets, a healthy environment, healthy food, ordinary human things, is most likely at least internally predisposed to a distorted perception of reality, and at the maximum is a suitable vessel for propaganda. Sociopathic predisposition seasoned with mathematical logic gives rise to truly monstrous images of stalking, which will only serve their own internal unknown purposes and will not reflect society's demands for mercy and ethics, or even the usual educational minimum.
The man who decided to attack me during the war, in which his compatriots kill and rape our women and children, and that the worst thing is rape our babies and sell video with this on the black market, when they burn our compatriots in mobile crematorias, I don’t say anymore about ordinary massacres and looting, at that time he is only interested in the Github commits of my repositories, which he wrote under my direction, has obviously become on the side of evil, and the only correct solution in this case is to completely put this person outside of my reality.
Have a nice investigation!
With honour, proud to be Ukrainian, yours Namdak Tonpa 🇺🇦