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, maintain civility and avoid the ad hominem logical fault. Yaniv256 (talk) 19:16, 24 July 2012 (UTC)'

My personal views as to why Mizar system external links are not in violation of Wikipedia policies and guidelines, previously here, have been relocated to my user space. Yaniv256 (talk) 13:48, 29 July 2012 (UTC)

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)

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)

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)

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)

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)

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)

The question of where and in what layout should we have this discussion is a classical red herring. Yaniv256 (talk) 22:12, 24 July 2012 (UTC)

The idea of formalized structures for communication should be obvious to a person who is intent on refining an article about a formal mathematical language. At Wikipedia, there is a general flow and practice to how Talk pages are used. If you want to redefine that just for here and just for you, you need to use the existing framework to get consensus for changing the framework to a new one. You cannot arbitrarily decide for a community what their framework will be, unless you are simply intent on disrupting communication. I suggest that for now, you use the framework being suggested, and if you wish to change it for the better, you set that aside as a secondary goal for the time being. -- Avanu (talk) 05:56, 25 July 2012 (UTC)

In my arrogant opinion your argument is true but suffers from a minor ad hominem flaw. Yet, carelessly, I fell for the scent and posted a good-hearted response on ANI. Thankfully, its true nature was quickly revealed. While we are on the off-topic I have an ancient koan for you to ponder: What is it exactly that makes us all express ourselves as if we originate from holy communion, while it is only the rest that are born out of sin? Yaniv256 (talk) 19:10, 26 July 2012 (UTC)

Because our eyes point outward, not inward. -- Avanu (talk) 06:06, 27 July 2012 (UTC)

I think this falls under WP:NOTDIRECTORY. I am however okay with the idea of links to Mizar and Matamath as an external entry for things like the axiom of choice or the continuum hypothesis where the axiom system matters a lot, mechanized reasoning seems something appropriate to point to there I think. It is not a yes no question applying to every branch of mathematics, proofs from axioms just are not the top level important thing in most other areas. Dmcq (talk) 08:53, 25 July 2012 (UTC)

There are several formalization projects (e.g. Mizar, Metamath, and MathWiki). Given that they are only of interest to a very small portion of readers, I don't believe it would be a good idea to start linking to these projects en masse from the External links section in all our mathematics articles. Perhaps they can be added as metadata when WikiData is finished next year. —Ruud 11:59, 25 July 2012 (UTC)

The WikiData idea seems a good one. I find the various existing standard links (wiktionary, wikiquote, wikisource) very useful as I know exactly what to expect so I of course don't use them unless I'm looking for precisely what they offer. Most often I ignore such links, as the only one I visit regularly wiktionary I visit to look up obscure words that aren't linked directly. But I'm sure some editors find them useful for the opposite reason: they often use them so are happy they are easy to find.--JohnBlackburne^words_deeds 01:15, 26 July 2012 (UTC)

I think this is a great idea. I posted an FYI on the MathWiki developer site. Yaniv256 (talk) 01:10, 26 July 2012 (UTC)

Would anyone mind if I revert my position and suggest to relocate this discussion to Wikipedia talk:Formalized math external links, where it may rest out of the way of discussions regarding the Mizar system article? I would also like to attach to this request a formal apology for all my breaches of talk page policy, guidelines and common practice. My apology. Yaniv256 (talk) 18:42, 28 July 2012 (UTC)

There's no need to move this discussion and it's best it stays here with its history and so incoming links to it are preserved. It's hardly too long and if the talk page fills up someone can archive it. The best thing would be to start another discussion with a broader focus, perhaps at the maths project talk page Wikipedia talk:WikiProject Mathematics, and link back to this one.--JohnBlackburne^words_deeds 20:51, 28 July 2012 (UTC)

I agree but feel I have been pushing this a little too much by myself. I really thought there would be some support for the idea. If anyone wishes to follow up on this advice please put a notice here to let us know. Yaniv256 (talk) 14:32, 29 July 2012 (UTC)

I would like to refine my proposal to address the issues raised. What I would like to propose is that we make an experiment. In this experiment we will select a small number of well chosen pages corresponding to key constructs in matching undergraduate math courses. We then ask some of the active professor editors to mention the links when teaching the relevant class and solicit responses by having the students make a general note whenever they use the link in the solution of a problem set. We gather the results and measure take-up quantitatively and by field. Suggested duration: 6 months. Yaniv256 (talk) 02:46, 26 July 2012 (UTC)

Automath lineage

I put it in the infobox that Mizar was influenced by Automath because it stands to reason, but I do not actually know this. Can anyone confirm? Also, does anyone have a release date? Yaniv256 (talk) 20:02, 29 July 2012 (UTC)

Ways this article can be improved

Does anyone have suggestions how I might improve this article? I could add some more information about the language, but I think a much longer article would be inconsistent with a notability consideration. Any ideas? Yaniv256 (talk) 16:09, 30 July 2012 (UTC)

External links modified (February 2018)

Hello fellow Wikipedians,

I have just modified one external link on Mizar system. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20111009115553/http://old.nabble.com/TPHOLs-becomes-ITP-(fwd)-td19435554.html to http://old.nabble.com/TPHOLs-becomes-ITP-%28fwd%29-td19435554.html
• Added {{dead link}} tag to http://foundations.cs.ru.nl/fndswiki/Research/MathWiki
• Added {{dead link}} tag to http://mws.cs.ru.nl/mwiki/

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 01:03, 3 February 2018 (UTC)