595:
585:
564:
320:
1008:. 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.
243:
222:
932:
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. --
191:
749:(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 Knowledge readers need to be made aware of formalized mathematical structures in the topic of the page they are reading? Do you think that
931:
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
Knowledge, 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
1150:
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.
1149:
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
1108:
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
1051:
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
744:
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
341:
700:
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
Knowledge readers are made aware of formalized mathematical structures in the topic of the page they are reading. Please read the
791:
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
1094:, 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.
1196:
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?
1129:
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.
153:
1052:
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.--
365:
651:
951:
505:
422:
360:
1363:
283:
293:
147:
693:
1368:
1296:
1292:
1278:
725:
My personal views as to why Mizar system external links are not in violation of
Knowledge policies and guidelines, previously here, have been relocated to
259:
1378:
1358:
641:
467:
79:
839:
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.--
1032:). 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
746:
726:
441:
1110:
895:
754:
617:
306:
250:
227:
1373:
835:
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
530:
85:
1236:
1120:
1059:
846:
799:
44:
831:
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
413:
1274:
When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.
608:
569:
394:
1091:
486:
99:
30:
104:
20:
168:
74:
135:
1339:
451:
332:
202:
461:
375:
65:
677:
external links on mathematical articles. To make the discussion concrete I am posting here the link I placed on the
753:
should also be linked in the same places? I suggest you start a discussion on the mathematics project talk page ...
496:
258:
related articles on
Knowledge. If you would like to participate, please visit the project page, where you can join
523:
1295:
to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the
129:
1330:
1228:
1036:
from the
External links section in all our mathematics articles. Perhaps they can be added as metadata when
109:
1173:
because it stands to reason, but I do not actually know this. Can anyone confirm? Also, does anyone have a
1224:
1005:
1237:
https://web.archive.org/web/20111009115553/http://old.nabble.com/TPHOLs-becomes-ITP-(fwd)-td19435554.html
125:
1314:
If you have discovered URLs which were erroneously considered dead by the bot, you can report them with
1302:
903:
750:
432:
208:
1227:. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit
594:
1240:
954:. Thankfully, its true nature was quickly revealed. While we are on the off-topic I have an ancient
894:
on that topic. The issue of whether it should be used on
Knowledge does not belong here. Probably
190:
175:
1115:
1054:
841:
794:
161:
55:
616:
on
Knowledge. If you would like to participate, please visit the project page, where you can join
1262:
1248:
1202:
1182:
1155:
1135:
1099:
1077:
975:
922:
876:
822:
779:
762:
734:
714:
600:
70:
1299:
before doing mass systematic removals. This message is updated dynamically through the template
584:
563:
1315:
351:
51:
899:
403:
255:
1322:
989:
937:
867:
operator is quite clear to me. In time, I, and perhaps others, will address all contested
814:
141:
1254:
890:
Whatever the merits or otherwise of the Mizar system, this page is for discussion of the
1281:, "External links modified" talk page sections are no longer generated or monitored by
1042:
1013:
963:
913:
The question of where and in what layout should we have this discussion is a classical
868:
836:
832:
477:
319:
1321:
If you found an error with any archives or the URLs themselves, you can fix them with
342:
Requested articles/Applied arts and sciences/Computer science, computing, and
Internet
1352:
1198:
1178:
1151:
1131:
1095:
1090:
Would anyone mind if I revert my position and suggest to relocate this discussion to
1073:
971:
918:
872:
818:
775:
758:
730:
710:
1220:
702:
689:
674:
24:
950:
flaw. Yet, carelessly, I fell for the scent and posted a good-hearted response on
1288:
914:
678:
613:
1287:. No special action is required regarding these talk page notices, other than
985:
947:
933:
706:
590:
1037:
896:
Wikipedia_talk:WikiProject_Mathematics#Mizar_system_external_links_discussion
1009:
810:
685:
384:
242:
221:
1170:
1025:
871:
articles. It might not be enough to convince you, but it will be there.
817:? They are close but only one draws the academic attention it deserves.
946:
In my arrogant opinion your argument is true but suffers from a minor
1344:
1206:
1186:
1159:
1139:
1124:
1103:
1081:
1063:
1046:
1017:
993:
979:
941:
926:
907:
880:
850:
826:
803:
783:
766:
738:
718:
1241:
http://old.nabble.com/TPHOLs-becomes-ITP-%28fwd%29-td19435554.html
1069:
1029:
955:
967:
460:
Find pictures for the biographies of computer scientists (see
184:
15:
1268:
673:
This section aggragates the arguments pro and con of placing
962:
that makes us all express ourselves as if we originate from
757:... for a sensible/agreed way of dealing with these topics.
1231:
for additional information. I made the following changes:
705:
article before posting, maintain civility and avoid the
1255:
http://foundations.cs.ru.nl/fndswiki/Research/MathWiki
1024:
There are several formalization projects (e.g. Mizar,
160:
1169:
I put it in the infobox that Mizar was influenced by
1068:
I think this is a great idea. I posted an FYI on the
612:, a collaborative effort to improve the coverage of
254:, a collaborative effort to improve the coverage of
1291:using the archive tool instructions below. Editors
809:Can I suggest a review of the distinction between
366:Computer science articles needing expert attention
966:, while it is only the rest that are born out of
33:for general discussion of the article's subject.
984:Because our eyes point outward, not inward. --
1277:This message was posted before February 2018.
506:WikiProject Computer science/Unreferenced BLPs
1092:Knowledge talk:Formalized math external links
174:
8:
423:Computer science articles without infoboxes
361:Computer science articles needing attention
1219:I have just modified one external link on
558:
327:Here are some tasks awaiting attention:
301:
216:
1364:High-importance Computer science articles
747:Category:Theorem proving software systems
1212:External links modified (February 2018)
669:Mizar system external links pro and con
560:
218:
188:
1111:Knowledge talk:WikiProject Mathematics
755:Knowledge talk:WikiProject Mathematics
268:Knowledge:WikiProject Computer science
1369:WikiProject Computer science articles
271:Template:WikiProject Computer science
7:
774:I posted an invitation to this page.
606:This article is within the scope of
248:This article is within the scope of
207:It is of interest to the following
23:for discussing improvements to the
442:Timeline of computing 2020–present
14:
1379:Low-priority mathematics articles
1359:C-Class Computer science articles
1223:. Please take a moment to review
1192:Ways this article can be improved
626:Knowledge:WikiProject Mathematics
468:Computing articles needing images
681:article external links section.
629:Template:WikiProject Mathematics
593:
583:
562:
318:
241:
220:
189:
45:Click here to start a new topic.
646:This article has been rated as
288:This article has been rated as
1113:, and link back to this one.--
958:for you to ponder: What is it
1:
620:and see a list of open tasks.
522:Tag all relevant articles in
262:and see a list of open tasks.
42:Put new text under old text.
1374:C-Class mathematics articles
1345:01:03, 3 February 2018 (UTC)
531:WikiProject Computer science
307:WikiProject Computer science
251:WikiProject Computer science
462:List of computer scientists
50:New to Knowledge? Welcome!
1395:
1308:(last update: 5 June 2024)
1269:http://mws.cs.ru.nl/mwiki/
1216:Hello fellow Wikipedians,
294:project's importance scale
1207:16:09, 30 July 2012 (UTC)
1187:20:02, 29 July 2012 (UTC)
1160:02:46, 26 July 2012 (UTC)
1140:14:32, 29 July 2012 (UTC)
1125:20:51, 28 July 2012 (UTC)
1104:18:42, 28 July 2012 (UTC)
1082:01:10, 26 July 2012 (UTC)
1064:01:15, 26 July 2012 (UTC)
1047:11:59, 25 July 2012 (UTC)
1018:08:53, 25 July 2012 (UTC)
1004:I think this falls under
994:06:06, 27 July 2012 (UTC)
980:19:10, 26 July 2012 (UTC)
942:05:56, 25 July 2012 (UTC)
927:22:12, 24 July 2012 (UTC)
908:16:53, 24 July 2012 (UTC)
881:19:09, 24 July 2012 (UTC)
851:18:42, 24 July 2012 (UTC)
827:18:31, 24 July 2012 (UTC)
804:16:38, 24 July 2012 (UTC)
784:16:27, 24 July 2012 (UTC)
767:15:48, 24 July 2012 (UTC)
739:13:48, 29 July 2012 (UTC)
719:19:16, 24 July 2012 (UTC)
696:formally proved about it.
645:
578:
524:Category:Computer science
300:
287:
274:Computer science articles
236:
215:
80:Be welcoming to newcomers
1040:is finished next year. —
652:project's priority scale
526:and sub-categories with
1070:MathWiki developer site
609:WikiProject Mathematics
688:of sigma-field in the
487:Computer science stubs
197:This article is rated
75:avoid personal attacks
898:is the right place.
751:Principia Mathematica
100:Neutral point of view
1289:regular verification
632:mathematics articles
305:Things you can help
105:No original research
1279:After February 2018
1333:InternetArchiveBot
1284:InternetArchiveBot
1109:project talk page
601:Mathematics portal
203:content assessment
86:dispute resolution
47:
1309:
1118:
1057:
892:Knowledge article
863:The notion of an
844:
797:
686:Formal definition
666:
665:
662:
661:
658:
657:
557:
556:
553:
552:
549:
548:
545:
544:
183:
182:
66:Assume good faith
43:
1386:
1343:
1334:
1307:
1306:
1285:
1266:
1252:
1165:Automath lineage
1114:
1053:
840:
793:
694:list of theorems
634:
633:
630:
627:
624:
603:
598:
597:
587:
580:
579:
574:
566:
559:
535:
529:
404:Computer science
333:Article requests
322:
315:
314:
302:
276:
275:
272:
269:
266:
265:Computer science
256:Computer science
245:
238:
237:
232:
228:Computer science
224:
217:
200:
194:
193:
185:
179:
178:
164:
95:Article policies
16:
1394:
1393:
1389:
1388:
1387:
1385:
1384:
1383:
1349:
1348:
1337:
1332:
1300:
1293:have permission
1283:
1260:
1246:
1229:this simple FaQ
1214:
1194:
1167:
1123:
1062:
1006:WP:NOTDIRECTORY
849:
815:formal language
802:
709:logical fault.
671:
631:
628:
625:
622:
621:
599:
592:
572:
541:
538:
533:
527:
515:Project-related
510:
491:
472:
446:
427:
408:
389:
370:
346:
290:High-importance
273:
270:
267:
264:
263:
231:High‑importance
230:
201:on Knowledge's
198:
121:
116:
115:
114:
91:
61:
12:
11:
5:
1392:
1390:
1382:
1381:
1376:
1371:
1366:
1361:
1351:
1350:
1327:
1326:
1319:
1272:
1271:
1257:
1243:
1235:Added archive
1213:
1210:
1193:
1190:
1166:
1163:
1147:
1146:
1145:
1144:
1143:
1142:
1119:
1116:JohnBlackburne
1087:
1086:
1085:
1084:
1066:
1058:
1055:JohnBlackburne
1021:
1020:
1002:
1001:
1000:
999:
998:
997:
996:
964:holy communion
888:
887:
886:
885:
884:
883:
856:
855:
854:
853:
845:
842:JohnBlackburne
798:
795:JohnBlackburne
789:
788:
787:
786:
742:
741:
698:
697:
670:
667:
664:
663:
660:
659:
656:
655:
644:
638:
637:
635:
618:the discussion
605:
604:
588:
576:
575:
567:
555:
554:
551:
550:
547:
546:
543:
542:
540:
539:
537:
536:
519:
511:
509:
508:
502:
492:
490:
489:
483:
473:
471:
470:
465:
457:
447:
445:
444:
438:
428:
426:
425:
419:
409:
407:
406:
400:
390:
388:
387:
381:
371:
369:
368:
363:
357:
347:
345:
344:
338:
326:
324:
323:
311:
310:
298:
297:
286:
280:
279:
277:
260:the discussion
246:
234:
233:
225:
213:
212:
206:
195:
181:
180:
118:
117:
113:
112:
107:
102:
93:
92:
90:
89:
82:
77:
68:
62:
60:
59:
48:
39:
38:
35:
34:
28:
13:
10:
9:
6:
4:
3:
2:
1391:
1380:
1377:
1375:
1372:
1370:
1367:
1365:
1362:
1360:
1357:
1356:
1354:
1347:
1346:
1341:
1336:
1335:
1324:
1320:
1317:
1313:
1312:
1311:
1304:
1298:
1294:
1290:
1286:
1280:
1275:
1270:
1264:
1258:
1256:
1250:
1244:
1242:
1238:
1234:
1233:
1232:
1230:
1226:
1222:
1217:
1211:
1209:
1208:
1204:
1200:
1191:
1189:
1188:
1184:
1180:
1176:
1172:
1164:
1162:
1161:
1157:
1153:
1141:
1137:
1133:
1128:
1127:
1126:
1122:
1117:
1112:
1107:
1106:
1105:
1101:
1097:
1093:
1089:
1088:
1083:
1079:
1075:
1071:
1067:
1065:
1061:
1056:
1050:
1049:
1048:
1045:
1044:
1039:
1035:
1031:
1027:
1023:
1022:
1019:
1015:
1011:
1007:
1003:
995:
991:
987:
983:
982:
981:
977:
973:
969:
965:
961:
957:
953:
949:
945:
944:
943:
939:
935:
930:
929:
928:
924:
920:
916:
912:
911:
910:
909:
905:
901:
897:
893:
882:
878:
874:
870:
866:
862:
861:
860:
859:
858:
857:
852:
848:
843:
838:
834:
830:
829:
828:
824:
820:
816:
812:
808:
807:
806:
805:
801:
796:
785:
781:
777:
773:
772:
771:
770:
769:
768:
764:
760:
756:
752:
748:
740:
736:
732:
728:
727:my user space
724:
723:
722:
720:
716:
712:
708:
704:
695:
691:
687:
684:
683:
682:
680:
676:
668:
653:
649:
643:
640:
639:
636:
619:
615:
611:
610:
602:
596:
591:
589:
586:
582:
581:
577:
571:
568:
565:
561:
532:
525:
521:
520:
518:
516:
512:
507:
504:
503:
501:
499:
498:
493:
488:
485:
484:
482:
480:
479:
474:
469:
466:
463:
459:
458:
456:
454:
453:
448:
443:
440:
439:
437:
435:
434:
429:
424:
421:
420:
418:
416:
415:
410:
405:
402:
401:
399:
397:
396:
391:
386:
383:
382:
380:
378:
377:
372:
367:
364:
362:
359:
358:
356:
354:
353:
348:
343:
340:
339:
337:
335:
334:
329:
328:
325:
321:
317:
316:
313:
312:
308:
304:
303:
299:
295:
291:
285:
282:
281:
278:
261:
257:
253:
252:
247:
244:
240:
239:
235:
229:
226:
223:
219:
214:
210:
204:
196:
192:
187:
186:
177:
173:
170:
167:
163:
159:
155:
152:
149:
146:
143:
140:
137:
134:
131:
127:
124:
123:Find sources:
120:
119:
111:
110:Verifiability
108:
106:
103:
101:
98:
97:
96:
87:
83:
81:
78:
76:
72:
69:
67:
64:
63:
57:
53:
52:Learn to edit
49:
46:
41:
40:
37:
36:
32:
26:
22:
18:
17:
1331:
1328:
1303:source check
1282:
1276:
1273:
1221:Mizar system
1218:
1215:
1195:
1175:release date
1174:
1168:
1148:
1041:
1033:
959:
891:
889:
864:
790:
743:
703:Mizar system
699:
690:Mizar system
675:Mizar system
672:
648:Low-priority
647:
607:
573:Low‑priority
514:
513:
497:Unreferenced
495:
494:
476:
475:
450:
449:
431:
430:
412:
411:
393:
392:
374:
373:
350:
349:
331:
330:
289:
249:
209:WikiProjects
171:
165:
157:
150:
144:
138:
132:
122:
94:
25:Mizar system
19:This is the
915:red herring
900:Deltahedron
679:sigma-field
623:Mathematics
614:mathematics
570:Mathematics
148:free images
31:not a forum
1353:Categories
1340:Report bug
948:ad hominem
707:ad hominem
692:, and the
1323:this tool
1316:this tool
1263:dead link
1249:dead link
811:gibberish
385:Computing
88:if needed
71:Be polite
21:talk page
1329:Cheers.—
1199:Yaniv256
1179:Yaniv256
1171:Automath
1152:Yaniv256
1132:Yaniv256
1096:Yaniv256
1074:Yaniv256
1038:WikiData
1034:en masse
1030:MathWiki
1026:Metamath
972:Yaniv256
919:Yaniv256
873:Yaniv256
819:Yaniv256
776:Yaniv256
759:Melcombe
731:Yaniv256
711:Yaniv256
433:Maintain
376:Copyedit
56:get help
29:This is
27:article.
1267:tag to
1253:tag to
1225:my edit
960:exactly
869:WP:ELNO
837:WP:ELNO
833:WP:ELNO
792:help.--
650:on the
414:Infobox
352:Cleanup
292:on the
199:C-class
154:WP refs
142:scholar
1259:Added
1245:Added
1028:, and
813:and a
395:Expand
205:scale.
126:Google
1121:deeds
1060:deeds
986:Avanu
934:Avanu
847:deeds
800:deeds
478:Stubs
452:Photo
309:with:
169:JSTOR
130:books
84:Seek
1203:talk
1183:talk
1156:talk
1136:talk
1100:talk
1078:talk
1043:Ruud
1014:talk
1010:Dmcq
990:talk
976:talk
956:koan
938:talk
923:talk
904:talk
877:talk
823:talk
780:talk
763:talk
735:talk
715:talk
284:High
162:FENS
136:news
73:and
1297:RfC
1239:to
968:sin
952:ANI
865:all
642:Low
176:TWL
1355::
1310:.
1305:}}
1301:{{
1265:}}
1261:{{
1251:}}
1247:{{
1205:)
1185:)
1177:?
1158:)
1138:)
1102:)
1080:)
1072:.
1016:)
992:)
978:)
970:?
940:)
925:)
917:.
906:)
879:)
825:)
782:)
765:)
737:)
729:.
721:'
717:)
534:}}
528:{{
156:)
54:;
1342:)
1338:(
1325:.
1318:.
1201:(
1181:(
1154:(
1134:(
1098:(
1076:(
1012:(
988:(
974:(
936:(
921:(
902:(
875:(
821:(
778:(
761:(
733:(
713:(
654:.
517::
500::
481::
464:)
455::
436::
417::
398::
379::
355::
336::
296:.
211::
172:·
166:·
158:·
151:·
145:·
139:·
133:·
128:(
58:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
