User talk:BlueSeaViolet

Welcome!

Hello, BlueSeaViolet, and welcome to Wikipedia! Thank you for your contributions. I hope you like the place and decide to stay. Here are some pages that you might find helpful:

I hope you enjoy editing here and being a Wikipedian! Please sign your messages on discussion pages using four tildes (~~~~); this will automatically insert your username and the date. If you need help, check out Wikipedia:Questions, ask me on my talk page, or ask your question on this page and then place {{help me}} before the question. Again, welcome!--MollyPollyRolly (talk) 18:46, 13 November 2021 (UTC)[reply]

Promoting ISA-AFP

Hello, BlueSeaViolet, and welcome to Wikipedia. We appreciate encyclopedic contributions, but all your contributions so far have been pointers to papers on ISA-AFP, which suggests that you are using WP to promote their work and are perhaps affiliated with them. Wikipedia does not allow this. For more information on this, please see:

They are interesting and relevant papers, but our COI and Promotion policies apply. In any case, the goal of Wikipedia is not to be a comprehensive bibliography on the topic of the article.

If you still have questions, there is a new contributors' help page, or you can click here to ask a question on my talk page. --Macrakis (talk) 19:24, 13 November 2021 (UTC)[reply]

Continued spamming

You have continued to add links to ISA-AFP after I informed you of our policies. Please do not add inappropriate external links to Wikipedia. Wikipedia is not a collection of links, nor should it be used for advertising or promotion. Inappropriate links include, but are not limited to, links to personal websites, links to websites with which you are affiliated (whether as a link in article text, or a citation in an article), and links that attract visitors to a website or promote a product. See the external links guideline and spam guideline for further explanations. Because Wikipedia uses the nofollow attribute value, its external links are disregarded by most search engines. If you feel the link should be added to the page, please discuss it on the associated talk page rather than re-adding it. Thank you. --Macrakis (talk) 21:23, 13 November 2021 (UTC)[reply]

Hello Macrakis:

The Archive of Formal Proofs is a *massive* database of formalised proofs (perhaps the largest) with contributors from all over the world. It includes proofs formalised in the widely used Isabelle proof assistant (:interactive theorem prover). The question is why you are trying to censor links to the Archive of Formal Proofs (?!!) All of my (few) Wikipedia contributions so far have been pointers to the Archive of Formal Proofs because this is a topic I know about. I am not "promoting" anything or anyone: I am contributing to Wikipedia what I know--which is what Wikipedia is about.

Please stop harassing me. BlueSeaViolet (talk) 21:26, 13 November 2021 (UTC)[reply]

To clarify: I am not doing anything in the list of things you are accusing me of: The links have nothing to do with "advertising" or "promotion": they are valid and very much related scientific contributions by a number of AFP contributors in the area of formalised mathematics. I find it very strange that you are trying to censor the Archive of Formal Proofs.BlueSeaViolet (talk) 21:38, 13 November 2021 (UTC)[reply]

BlueSeaViolet, I understand that the Archive of Formal Proofs is a high-quality collection of formal proofs (and it is discussed in Isabelle (proof assistant)). But that's not the question. The question is whether links to the AFP articles belong in the External Links section. There are many refereed articles about, say, octonions, and WP only includes a small, select number of them.

Also, please read our policy assume good faith. Just because you disagree with me does not mean that you should accuse me of "censoring links" and "harassing" you. I am trying to apply WP policy as I understand it. If, after reading the above statements of policy, you disagree, there are various dispute resolution mechanisms. --Macrakis (talk) 21:53, 13 November 2021 (UTC)[reply]

Hello again Macrakis:

You have falsely accused me of "spamming" (!) and posting links for "promotion" (!) or "advertising" (!) These accusations are completely unfounded and you owe me an apology. I have carefully read the list of guidelines you sent and I have not broken any of the rules you have listed. Yes, of course there are many refereed articles on these topics, but here we are not talking about articles--this is something different: We are talking about *formal proof developments* which is a huge area in its own right and has been blooming in recent years. It is fit for any central theorem or important mathematical topic to have a link to its respective formalisation in a proof assistant (if there exists any). Not only do the AFP links belong there, but they are also necessary. In this case, these are formalisations in the proof assistant Isabelle/HOL, but the same is true about formalisations in other proof assistants like Agda, Lean, etc..(if any such formalisations even exist at all). These formalisations are important and highly sophisticated pieces of work. If you do not personally like formalised mathematics (or the proof assistant Isabelle/HOL), this may be your personal taste but this does not make this huge area any less relevant or significant and it is certainly not a reason to delete the Archive of Formal Proofs links.BlueSeaViolet (talk) 23:02, 13 November 2021 (UTC)[reply]

I am sorry if I misunderstood your motives. When I see a new user whose only activity is systematically adding links to multiple articles, all going to one outside site, it certainly "smells" like spamming. I understand that formal proof developments are an important area, and I certainly have nothing against them. Indeed, I have a great deal of admiration for Gérard Huet, whom I was lucky to meet many decades ago at Rocquencourt.

You say that AFP links are "necessary" on all mathematical topics where they exist. That may well be true, but it might be good to establish a consensus about it on, say, Wikipedia talk:WikiProject Mathematics, before adding large numbers of ELs which might be reverted.

Also, by the way, you might want to familiarize yourself a bit more with some of our conventions here. For example, for links to Wikipedia pages, we never use the syntax [https://en.wikipedia.org/wiki/Lawrence_Paulson Paulson, L. C.], but rather [[Lawrence Paulson|Paulson, L. C.]]. You should also indent your answers to other people's comments on Talk pages using ":". --Macrakis (talk) 00:13, 14 November 2021 (UTC)[reply]

Thank you for your reply. Yes, I just joined Wikipedia less than a day ago: it never crossed my mind that my edits could be regarded

as anything even remotely related to spamming as the Archive of Formal Proofs is not a private site or a private or for profit organisation, it's a huge open-source database with hundreds of contributors.

I added less than 10 AFP links and this was because formalised mathematics is an area I am interested in and I know a few things about: if I knew something about e.g. gardening I would be editing gardening pages instead. So I don't see why it is strange for an editor to focus on adding things about a specific topic they know something about-as far as I understand Wikipedia is all about sharing what each of us can share in their area(s) of interest.

(And even if I wanted to contribute to another topic I wouldn't have found the time for any other activity just yet-I just joined less than a day ago!)

Thank you for suggesting to discuss adding formal proofs links on Wikipedia talk:WikiProject Mathematics . This is a great idea and I will do so as soon as I find the free time to go back to editing Wikipedia (this will probably be after several days). With this opportunity I would like to encourage other editors to join in adding links to formalisations (not necessarily only from the Archive of Formal Proofs but also perhaps from other databases too containing proofs formalised in different proof assistants as well, if they exist). Thank you for your tips about editing conventions, it's useful to know.

BlueSeaViolet (talk) 02:24, 14 November 2021 (UTC)[reply]

Sadly, the fact that an organization is open-source, non-profit, and serious doesn't mean that links to its content can't be spam. Every so often, some legitimate academic researcher will start adding links to their own published work, which is strongly discouraged under WP:COI. In at least one case, they were so aggressive about adding their links to tangentially related articles that they had to be banned from WP.

In your case, the "red flag" was that instead of replying to my removal of the link on octonion in the Talk:Octonion page, you just reinstated it. And then you continued to add links to AFP without replying to my notification on your talk page where I invited you to discuss the issue.

WP has not just content norms, but also behavioral norms, which admittedly take some time to learn. You might want to review WP:BRD, for example.

I look forward to your future contributions! I know it takes some time to learn the ropes (my first edits were also reverted... in 2004), but WP is a great place to share knowledge. --Macrakis (talk) 16:09, 14 November 2021 (UTC)[reply]

I see- I understand your concerns. I reverted your removal because (not knowing anything about the Talk pages yet-having joined literally some minutes before) I thought that was the "expected"/"normal" way of responding to an edit. I added a short comment saying that the linked material is indeed very relevant to the topic and notable and I thought that answer would be considered enough.

As I said, I was genuinely surprised to see that an Archive of Formal Proofs link containing the respective proof-assistant formalisation of mathematical material on the very exact topic of the specific Wikipedia page was deemed as "inappropriate" or "promoting".

I did not know about the "Talk" pages until you explained in more detail and it took me a while to figure out how to answer to messages, hence my delay. Thank you for letting me know about the "Talk" pages and the norms and conventions: this is really useful! (I will be contributing to mathematics, formal mathematics and engineering but I expect I will have free time to do so on Saturdays only). BlueSeaViolet (talk) 19:22, 14 November 2021 (UTC)[reply]

BlueSeaViolet, you are invited to the Teahouse!

Hi BlueSeaViolet! Thanks for contributing to Wikipedia.
Be our guest at the Teahouse! The Teahouse is a friendly space where new editors can ask questions about contributing to Wikipedia and get help from experienced editors like Lectonar (talk).

Visit the Teahouse

We hope to see you there!

Delivered by HostBot on behalf of the Teahouse hosts

16:01, 14 November 2021 (UTC)