Talk:Mizar system

Mizar system external links pro and con

This section aggragates the arguments pro and con of placing Mizar system external links on mathematical articles. To make the discussion concrete I am posting here the link I placed on the sigma-field article external links section.

• Formal definition of sigma-field in the Mizar system, and the list of theorems formally proved about it.

I do hope we can have some productive discussion about these issues, as I am sure that together we can improve the way in which Wikipedia readers are made aware of formalized mathematical structures in the topic of the page they are reading. Please read the Mizar system article before posting, keep to the discussion exsisting layout, maintain civility and avoid the ad hominem logical fault. Yaniv256 (talk) 19:16, 24 July 2012 (UTC)

WP:EL

Pro: WP:EL states that "some acceptable links include those that contain further research that is accurate and on-topic, information that could not be added to the article for reasons such as copyright or amount of detail, or other meaningful, relevant content that is not suitable for inclusion in an article for reasons unrelated to its accuracy". The formal definition of sigma-field and the collection of proofs that have been formalized on it is on-topic on the sigma-field page. It cannot be added to the article because the amount of detail and form of presentation would overwhelm the typical reader. However, it is of interest to current mathematics and computer science students in the advanced undergraduate and graduate level, as it allows them to sort out exactly what a sigma field is and how its properties are proved in absolute rigor.

Con:

WP:ELNO.1

Con: WP:ELNO.1 states that linking to "any site that does not provide a unique resource beyond what the article would contain if it became a featured article" should be avoided.

Pro: Clearly, a sigma-field featured article would not contain the body of all formalized proofs on sigma-fields. It may contain the formalized definition, one day in the future, if and when the formal language in which it is stated becomes commonly used in higher education.

WP:ELNO.7

Con: WP:ELNO.7 recommends that one should generally avoid "Sites that are inaccessible to a substantial number of users, such as sites that only work with a specific browser or in a specific country".

Pro: The links provided should work in most browsers and countries. They do not require an academic library proxy, so they are more accessible than most scientific publications.

WP:ELNO.9

Con: WP:ELNO.9 recommends that one should generally avoid "Links to any search results pages, such as links to individual website searches, search engines, search aggregators, or RSS feeds".

Pro: Yes, that it is correct. The list of theorems is generated ad-hoc by a search engine. But, one would have to look at the code to know that. The argument is that the content which is provided does not resemble a search engine result. And, that it is the content of the page linked that WP:ELNO.9 refers to.

WP:ELNO.13

Con: WP:ELNO.13 states that "the link should be directly related to the subject of the article. A general site that has information about a variety of subjects should usually not be linked to from an article on a more specific subject ... If a section of a general website is devoted to the subject of the article, and meets the other criteria for linking, then that part of the site could be deep linked".

Pro: Agreed. The suggested insertion includes one internal off-topic link, the Mizar system link, that is needed in order to introduce the two on-topic external deep links.

Mizar links and gibberish

Con: External links should provide something recognizably useful to the topic of the page: these external links just lead to gibberish. Some abstract scheme for proving things related to sigma-fields is not directly connected to sigma-fields. Consider all the other similar schemes described in Category:Theorem proving software systems (and similar categories)... are all of these to be mentioned in every mathematical article? I don't see any of these as having been treated in the way you are trying. Why do you think that Wikipedia readers need to be made aware of formalized mathematical structures in the topic of the page they are reading? Do you think that Principia Mathematica should also be linked in the same places? I suggest you start a discussion on the mathematics project talk page ...Wikipedia talk:WikiProject Mathematics ... for a sensible/agreed way of dealing with these topics. Melcombe (talk) 15:48, 24 July 2012 (UTC)

I posted an invitation to this page.Yaniv256 (talk) 16:27, 24 July 2012 (UTC)

Con: They are gibberish to me to. I've come here from the maths project page and have never heard of the Mizar system, which I think will be true of most readers. So they are not useful links, and are likely to confuse far more readers than they help.--JohnBlackburne^words_deeds 16:38, 24 July 2012 (UTC)

Pro: Can I suggest a review of the distinction between gibberish and a formal language? They are close but only one draws the academic attention it deserves. Yaniv256 (talk) 18:31, 24 July 2012 (UTC)

Con: You can suggest but no-one here is going to spend hours studying a brand new language to evaluate the links. And you've misunderstood how WP:ELNO works. You don't pick out individual entries in that list to support a link, a link has to pass them all; if it fails just one then it fails WP:ELNO and these link fail #7: Sites that are inaccessible to a substantial number of users while the second one fails #9, Links to any search results pages.--JohnBlackburne^words_deeds 18:42, 24 July 2012 (UTC)

Pro: The notion of an all operator is quite clear to me. In time, I, and perhaps others, will address all contested WP:ELNO articles. It might not be enough to convince you, but it will be there. Yaniv256 (talk) 19:09, 24 July 2012 (UTC)

Best place to have this discussion

Whatever the merits or otherwise of the Mizar system, this page is for discussion of the Wikipedia article on that topic. The issue of whether it should be used on Wikipedia does not belong here. Probably Wikipedia_talk:WikiProject_Mathematics#Mizar_system_external_links_discussion is the right place. Deltahedron (talk) 16:53, 24 July 2012 (UTC)