Letter.md

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:

1. https://github.com/groupoid/anders/graphs/contributors
2. https://github.com/groupoid/homotopy.dev/graphs/contributors
3. https://github.com/groupoid/ivy.mike/graphs/contributors,

but not in

1. https://github.com/groupoid/principia/graphs/contributors
2. https://github.com/groupoid/ground.zero/graphs/contributors
3. https://github.com/groupoid/castle.bravo/graphs/contributors
4. https://github.com/groupoid/hurricane/graphs/contributors
5. https://github.com/groupoid/smiling.buddha/graphs/contributors
6. 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

1. this work was paid
2. @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

wasted

@forked-from-1kasper according your info you are from па_russia
So for this reason you could go in the same direction as your warship, I mean fuck yourself.

Attaching image to clarify the direction

I have tons of evidence from #CHLOR channel where russian fascism took its place, @forked-from-1kasper was intentionally humiliating ukrainins under the nickname of Hitler after a series of warnings. Think of that choice. BRATISLAVA is @Borschemancer and justperson is @slaykovsky, the @facebook employee.

2021-08-09 14:14:50 | _dristcord2 | <BRATISLAVA#7523> хохол = фашист
2021-12-08 13:32:30 | dristcord | <justperson#9703> Ты хохол
2021-12-25 12:11:59 | dristcord | <Hitler#4876> в ответ пишут, что автор заявления — хохол
2021-12-25 12:11:59 | dristcord | <Hitler#4876> в ответ пишут, что автор заявления — хохол
2022-01-04 17:47:40 | dristcord | <Hitler#4876> JoJo_Rabbit_d3 попався, хохол
2022-01-08 17:08:58 | dristcord | <Guest_1488#0000> (или хохол)
2022-02-03 15:03:11 | dristcord | <BratocqNeTravi#0000> ну или как типичный хохол
2022-02-07 16:12:33 | dristcord | <Bandera#0000> anon516: попався, хохол

https://github.com/groupoid/anders/blob/main/ACKNOWLEDGEMENT#L6

I think these accounts should be banned from @github permanently

OR

https://tonpa.guru/stream/2022/2022-03-15%20Github%20supports%20Russian%20Fascism.htm

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 🇺🇦

@5HT

First of all, thank you for starting to answering concretely instead of abstract insults and threats.
But from now on I’m not going to respond to your insults and obvious provocations, because I don’t see it as any kind of constructive dialogue.

You're young … and you can't change the fact that you were sponsoring and supporting the war.

Wait, how much of your money paid to me (and not only to me) went to the taxes of the Russian Federation? Or this is something different? The economy just doesn’t work the way you describe.

https://tonpa.guru/stream/2022/2022-03-15%20Github%20supports%20Russian%20Fascism.htm

You announced a few weeks ago that you were leaving GitHub, but since then you’ve only been committing more? How?

I taught him Modal HoTT after visiting Geometry in Modal HoTT workshop…

Lol, what? Please proofs or don’t lie. I’ve already elaborated on Twitter how incompetent you are in this field, so please stop the lying. Participating in a workshop doesn’t mean you have learned anything at all.

Now he is saying that everything he made was made by him alone…

Read my posts carefully, I wrote it clearly:

his commits are mainly about library, *.anders files, of language, but not about language itself, i.e. *.ml files

Are you going to argue with that?

Your contribution will be completely swiped out.

So you will delete “src/” directory, “framework.js” (if you remember, it was my idea: forked-from-1kasper/homotopy.dev@7975f1c), https://github.com/groupoid/bertrand and https://github.com/groupoid/valery?

This is not ISC, this is new license. Please respect that!

I see, but this license cannot work backwards in time. Moreover, I’m not a lawyer, but something tells me that you can’t change ISC to another license without asking everyone involved in project.

…trying to steal my accounts…

I don’t understand, what’s the point of me hacking your accounts? All the facts proving my point are in the public access on GitHub and are available to everyone.

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.

???

but there is no evidence EXE code was written by anyone execpt me
full history 848 commits

No
one
except
you?

You are the person who is spreading misinformation about me for 44 days starting from day 1…

From February 24? As I said, “I worked… until February 28”. What did I post from February 24 to 28?

I'm still fighting in twitter with trolls from your #CHLOR channel

That’s a real paranoia, you see russian trolls everywhere (even among your Ukrainian fellow citizens) and even Russian Federal Security Service majors, whose activities are aimed at bullying you. You’re just an ordinary programmer from Kyiv, where did you get such an inflated ego?

That is you who called us … on our HOMOTOPY.DEV channel publicly

Your baseless claims that I’ve insulted someone sound pretty strange, considering how many of your posts are available, where you’ve been throwing mud at me without restricting your language. Unlike you, I haven’t done that, I’ve always advocated open dialogue and in our discussion of this word I openly expressed my opinion. Being aware of your and other chat participants morbid attitude to this word, I have never used it in their (including you) direction.

He is maybe thinking that I'm like him 19 y.o. who want to have text battles in Internet.

Is that why you’re answering?

This is not true, you can see my public life in all social networks

Yea‐ah, I’ve seen.

Я НЕ ВЕДУ ДИАЛОГОВ С ТЕРРОРИСТАМИ
ПРОСТО ПОШЕЛ НАХУЙ
ТЫ ПРОСТО БОЛЬНОЕ НИЧТОЖЕСТВО

TWIMC. You can obtain EXE code by performing:

git clone https://github.com/5HT/exe-archive

This is very first prototype of syntax and initial point of Anders/Erlang, full code:

├── README.md
├── priv
│   ├── cubical.syntax
│   ├── inductive.ctt
│   ├── mltt.ctt
│   └── trunc.ctt
├── rebar.config
├── src
│   ├── cub.app.src
│   ├── cub.erl
│   ├── cub_lexer.xrl
│   ├── cub_parser.yrl
│   └── macro.erl
└── sys.config

Nobody did this except me as you see by commits. Andy was learning HoTT by implementing Awodey's Impredicative Encoding which is now part of Anders/OCaml library. Paul was working on Lean modeling and previous EXE syntax that has nothing common with cubicaltt, which is reference point for Anders/OCaml, so Paul' code was removed. Denys was learning cubicaltt with System-F realization of recursive schemes, which was excluded from Anders, but included by me in cubicaltt. Other contributors were proofreaders.

This person @forked-from-1kasper is writing letters to Henk Barendregt, tagging famous mathematicians on twitter, trying to discredit, attacking on Ukrainian mathematical community Groupoid Infinity. Uneffectfully. This is insane behavior in the middle of war with Ukraine. I have many tasks here in developing products for Ukrainian Government in position of Enterprise Architect, this is just another attack surface in Great Patriotic War. Also I have the dignity and duty to protect Groupoid Infinity from russian attacks.

The presentation of my CCHM library was made in CMU in 2019, long before Anders was started. I decided to switch to OCaml version and invited @forked-from-1kasper to my repositories. ISC License with this little fascist was added by me only in 6 JUL 2021 as a gift, after Anders release. Only from that point he can start pretending to something and only in US jurisdiction, while Groupoid Infinity has Ukrainian jurisdiction.

Anders/OCaml was funded by Ministry of Internal Affairs of Ukraine and Synrc Research Center. I'm the sole copyright holder of N2O.DEV and ERP.UNO the main products of Synrc Research. Synrc Research operates since 2005 and my code is powering PrivatBank, the biggest bank in Eastern Europe with 30 millions of retail subscribers, MIA products and its infrastructure, messaging platforms, and many more small businesses. But also it powers russian and blockchain businesses. After Full Scale War of russian orks against The Brave People of Dignity I'm changing licenses of all my repositories to DHARMA LICENSE to aviod this ridicuouls misundestanding of General Ethics. From now on my code will not power any russians or blockchains.

Anders is a product of Synrc Research that was started for the sake of formalization of enterprise protocols and modalities (Guarded Cubical, Flat, de Rham and other modalities). Our specification of N2O, KVS, BPE and NITRO library is given in Anders language. At the bottom of the page you can obtain companies who use our technologies. Our stack is available for most functional languages: https://n2o.dev/tech/ The full picture is rendered in my PhD dissertation:

• Formal runtime environment, system of formal languages and base libraries for programming, theorem proving and formal philosophy.
• Groupoid Infinity FORMAL.UNO monography.pdf

We are considering here this is as an attack to our infrastructure, our reputation and our merits! All Anders articles and educational materials were written by myself alone. I claim I can implement Anders in any language in 1 week. Invite me on your site and I will prove that.

• Maxim Sokhatsky. HoTT: The language of Space. Presentation of CCHM and cubicaltt 26-09-2018
• Maxim Sokhatsky. Презентація кубічного CCHM прувера Anders 0.7.2 від Групоїд Інфініті. 2021-07-18
• Maxim Sokhatsky. Anders: верификатор математики. 2022-01-17
• Maxim Sokhatsky. Anders: Modal Homotopy Type System. 2022-01-17

Have a nice evening!
With honour, proud to be Ukrainian, yours Максим Еротейович Сохацький 🇺🇦

FULL UPDATED VERSION OFFICIALY:

https://tonpa.guru/stream/2022/2022-04-10%20Russian%20War%20against%20Groupoid%20Infinity.htm

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.

For example: in groupoid/pure, you can see from the commits how the authors of the project disappeared: Andy Melnikov, Paul Lyutko.

Just to clarify, nponeccop and Andy Melnikov are the same person.

I didn't work for money, instead I voluntarily sponsored a few months of Paul's work. I'm a humble and a relatively wealthy person, and all those details (who hired whom) were just unimportant for me back then. I saw this monetary contribution as voluntary token amount to motivate Paul, the late fact that both @5HT and Paul considered it salary came as a surprise to me.

As for "contributions being erased", both my and Paul's work were independent subprojects. Neither of us finished the respective subproject, so our contribution was in some sense "useless" and later @5HT deleted the code he didn't see as relevant anymore. Subsequently, he removed my name from the website, and I just didn't care.

During my work I extensively refactored the "standard library", and it's not clear whether my code is still there in the "upstream" repo of @5HT. Again, I just don't care. My code remains in my github fork and I can continue the work any time if I feel like it. My subproject was essentially a formalization of proofs in one paper, so at this point it's a completely different project from what @5HT does.

Thank you for your support, Andy! Still love you so much!

Since I was tagged in the Twitter discussion.

@5HT

You're young fascist and you can't change the fact that you were sponsoring and supporting the war.

by paying taxes on the money that you had been sending to Russia for 4 years knowing full well where the money was going to? By that logic (not my logic) you are the source of the sponsorship.

@5HT, you say that

@forked-from-1kasper was intentionally humiliating ukrainins under the nickname of Hitler after a series of warnings

Are there any proofs of this? I mean, I can see the log, but it's not obvious for me that Hitler and @forked-from-1kasper is the same person

@forked-from-1kasper Stop with it now, you are a crazy man. Stops cry, begins contribute with the world like the @5HT