158:
101:
957:. In these systems the logical core is a library of their programming language. Theorems represent new elements of the language and can only be introduced via "strategies" which guarantee logical correctness. Strategy composition gives users the ability to produce significant proofs with relatively few interactions with the system. Members of the family include:
57:
2020:
1111:
Freek
Wiedijk has been keeping a ranking of proof assistants by the amount of formalized theorems out of a list of 100 well-known theorems. As of September 2023, only five systems have formalized proofs of more than 70% of the theorems, namely Isabelle, HOL Light, Coq, Lean, and Metamath.
947: â Allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification.
1226:
1003:
is an interactive theorem prover, successor of HOL. The main code-base is BSD-licensed, but the
Isabelle distribution bundles many add-on tools with different licenses.
1669:
941: â a programming language, a first-order logical theory, and a theorem prover (with both interactive and automatic modes) in the BoyerâMoore tradition.
1891:
38:
1987:
1906:
1757:
1356:
2042:
1834:
600:
122:
1318:
1042:
2190:
1703:
2103:
2068:
1961:
321:
144:
2170:
1787:
1686:
2108:
1283:
331:
2130:
1054:
856:
2185:
1096:
613:
555:
544:
189:, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a
157:
1728:
Licata, Daniel R.; Shulman, Michael (2013). "Calculating the
Fundamental Group of the Circle in Homotopy Type Theory".
1186:
2146:
356:
312:
2050:
2046:
2030:
1858:
115:
109:
1063:
and ETPS â Interactive theorem provers also based on simply-typed lambda calculus, but based on an independent
580:
263:
1156:
1103:
extensions have been developed for Coq, Isabelle by
Makarius Wenzel, and for Lean 4 by the leanprover developers.
2195:
1293:
1259:
447:
430:
213:
126:
69:
45:
1912:
161:
An interactive proof session in CoqIDE, showing the proof script on the left and the proof state on the right
1265:
1121:
1081:
1000:
763:
694:
592:
197:
1060:
1017:
1012:
682:
638:
258:
248:
1545:
325:
906:
646:
1202:
604:
75:
2120:
1971:
1271:
690:
31:
1813:
1763:
1735:
1639:
1505:
1423:
1143:
1100:
954:
950:
826:
650:
438:
238:
170:
1607:
1464:
1983:
1975:
1957:
1902:
1753:
1352:
1297:
1169:
1038:
972:
864:
185:
by humanâmachine collaboration. This involves some sort of interactive proof editor, or other
1126:
The following is a list of notable proofs that have been formalized within proof assistants.
2135:
1949:
1745:
1657:
1629:
1619:
1497:
1344:
282:
253:
166:
27:
Software tool to assist with the development of formal proofs by humanâmachine collaboration
1707:
1682:
1378:"agda/agda: Agda is a dependently typed programming language / interactive theorem prover"
1333:
17:
2125:
1887:
1678:
1006:
1998:
74:
Please expand the article to include this information. Further details may exist on the
1923:
944:
902:
392:
243:
209:
186:
1661:
2179:
1944:
Pfenning, Frank (1996). "The practice of logical frameworks". In
Kirchner, H. (ed.).
1277:
596:
588:
278:
1643:
1332:
Hunt, Warren; Matt
Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith (2005).
1927:
1767:
1509:
1034:
963: â The "primary descendant", still under active development. Support for both
755:
182:
1402:
1948:. Lecture Notes in Computer Science. Vol. 1059. Springer. pp. 119â134.
1319:"Quanta Magazine â How Close Are Computers to Automating Mathematical Reasoning?"
1122:
Computer-assisted proof § Theorems proved with the help of computer programs
2087:
1238:
989:
911:
869:
831:
768:
700:
609:
519:
287:
1729:
1439:
1624:
2171:
Science: Math: Logic and
Foundations: Computational Logic: Logical Frameworks
1953:
1566:
1280: â Proposal for a computer-based database of all mathematical knowledge
1274: â Proving or disproving the correctness of certain intended algorithms
978:
964:
472:
2150:
988:
ProofPower â Went proprietary, then returned to open source. Based on
56:
2082:
1051: â A proof assistant based on higher-order logic which is eXtensible.
2140:
1749:
1530:
1064:
725:
190:
1348:
1025: â A light system based on the Calculus of Inductive Constructions.
2097:
1501:
1343:. Lecture Notes in Computer Science. Vol. 3603. pp. 163â178.
1289:
968:
1634:
1485:
1099:
infrastructure for document-oriented proof processing. More recently,
1469:
1173:
1057:(PVS) â a proof language and system based on higher-order logic.
1028:
1022:
736:
1704:"Feit thomson proved in coq - Microsoft Research Inria Joint Centre"
2049:
external links, and converting useful links where appropriate into
1835:"'A-Team' of Math Proves a Critical Link Between Addition and Sets"
1818:
1592:
1427:
1268: â Mathematical proof at least partially generated by computer
656:
1740:
1484:
Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier (1993).
1092:
1077:
982:
894:
818:
793:
483:
442:
405:
400:
367:
156:
2166:
1788:"Math Problem 3,500 Years In The Making Finally Gets A Solution"
1731:
2013 28th Annual ACM/IEEE Symposium on Logic in
Computer Science
1048:
960:
938:
508:
270:
1982:. Studies in Logic. Vol. 137. Elsevier. pp. 683â786.
1377:
2013:
1262: â Subfield of automated reasoning and mathematical logic
1088:
94:
50:
1031: â A proof assistant based on first-order minimal logic.
2100:(with a general introduction to interactive theorem proving)
196:
A recent effort within this field is making these tools use
1037: â A proof assistant based on first-order logic, in a
1812:
Avigad, Jeremy (2023). "Mathematics and the formal turn".
2038:
2033:
may not follow
Knowledge (XXG)'s policies or guidelines
200:
to automate the formalization of ordinary mathematics.
1091:. Isabelle includes Isabelle/jEdit, which is based on
953: â A family of tools ultimately derived from the
320:
Ulf Norell, Nils Anders
Danielsson, and Andreas Abel (
1205:
1067:
of the logical theory and independent implementation.
181:
is a software tool to assist with the development of
1976:"X. Types in computer science, philosophy and logic"
1897:. In Robinson, Alan J. A.; Voronkov, Andrei (eds.).
1892:"18. Proof-assistants using Dependent Type Systems"
1286: â Logical problem studied in computer science
1220:
2147:"Specific Logical Frameworks and Implementations"
2136:Database of Existing Mechanized Reasoning Systems
1486:"IMPS: An interactive mathematical proof system"
1076:A popular front-end for proof assistants is the
2131:Theorem Proving and Automated Reasoning Systems
997:IMPS, An Interactive Mathematical Proof System.
1935:
1608:"Proof assistants: History, ideas and future"
1372:
1370:
1368:
1087:Coq includes CoqIDE, which is based on OCaml/
8:
1670:Notices of the American Mathematical Society
1946:Trees in Algebra and Programming â CAAP '96
214:Automated theorem proving § Comparison
2104:Interactive Theorem Proving for Agda Users
2092:Certified Programming with Dependent Types
30:For verification in computer science, see
2069:Learn how and when to remove this message
1901:. Vol. 2. Elsevier. pp. 1149â.
1817:
1739:
1633:
1623:
1212:
1208:
1207:
1204:
1199:Polynomial Freiman-Ruzsa conjecture over
516:Michael Norrish, Konrad Slind, and others
145:Learn how and when to remove this message
2121:Digital Math by Category: Tactic Provers
1465:"Release v0.198 ¡ metamath/Metamath-exe"
1128:
217:
108:This article includes a list of general
39:Interactive Theorem Proving (conference)
2098:Introduction to the Coq Proof Assistant
1309:
1080:-based Proof General, developed at the
2126:Automated Deduction Systems and Groups
1341:Theorem Proving in Higher Order Logics
981: â A thriving "minimalist fork".
1859:"We have proved "BB(5) = 47,176,870""
1662:"Formal ProofâThe Four-Color Theorem"
7:
1999:"The Seventeen Provers of the World"
1591:Wiedijk, Freek (15 September 2023).
1533:. July 29, 2024 – via GitHub.
1422:Search for "proofs by reflection":
1317:Ornes, Stephen (August 27, 2020).
114:it lacks sufficient corresponding
25:
1606:Geuvers, Herman (February 2009).
37:For the academic conference, see
2018:
1298:first-order and equational logic
1221:{\displaystyle \mathbb {F} _{2}}
210:Dependent type § Comparison
99:
55:
2109:A list of theorem proving tools
1899:Handbook of Automated Reasoning
1692:from the original on 2011-08-05
2004:. Radboud University Nijmegen.
1490:Journal of Automated Reasoning
1284:Satisfiability modulo theories
1043:TarskiâGrothendieck set theory
1:
1055:Prototype Verification System
1833:Sloman, Leila (2023-12-06).
1706:. 2016-11-19. Archived from
18:Interactive theorem proving
2212:
1890:; Geuvers, Herman (2001).
1593:"Formalizing 100 Theorems"
1119:
207:
179:interactive theorem prover
43:
36:
29:
2191:Automated theorem proving
1863:The Busy Beaver Challenge
1625:10.1007/s12046-009-0001-5
1260:Automated theorem proving
1137:
1134:
1131:
1116:Notable formalized proofs
232:
229:
226:
223:
220:
1980:Handbook of Proof Theory
1978:. In Buss, S. R. (ed.).
1954:10.1007/3-540-61064-2_33
1928:"17. Logical frameworks"
1334:"Meta Reasoning in ACL2"
1294:automated theorem prover
70:automated proof checking
46:Interactive proof system
44:Not to be confused with
1997:Wiedijk, Freek (2005).
1266:Computer-assisted proof
1082:University of Edinburgh
585:Isabelle2024 (May 2024)
513:Kananaskis-13 (or repo)
230:Implementation language
198:artificial intelligence
129:more precise citations.
1440:"Lean 4 Releases Page"
1222:
162:
66:is missing information
2083:Theorem Prover Museum
1939:. pp. 1065â1148.
1531:"coq-community/vscoq"
1223:
1157:FeitâThompson theorem
160:
2163:(By Frank Pfenning).
2141:NuPRL: Other Systems
2039:improve this article
1972:Constable, Robert L.
1750:10.1109/lics.2013.28
1734:. pp. 223â232.
1203:
1187:ErdĹsâGraham problem
1107:Formalization extent
764:BiaĹystok University
387:Not yet Implemented
2186:Argument technology
2051:footnote references
1936:Handbook vol 2 2001
1349:10.1007/11541868_11
1272:Formal verification
1009: â Java based.
951:HOL theorem provers
351:Already executable
307:Already executable
259:Proof by reflection
32:formal verification
1544:Wenzel, Makarius.
1502:10.1007/BF00881906
1218:
1144:Four color theorem
1101:Visual Studio Code
955:LCF theorem prover
827:Cornell University
651:Microsoft Research
439:Microsoft Research
239:Higher-order logic
171:mathematical logic
163:
2079:
2078:
2071:
1989:978-0-08-053318-6
1908:978-0-444-50812-6
1759:978-1-4799-0413-6
1677:(11): 1382â1393,
1658:Gonthier, Georges
1358:978-3-540-28372-0
1251:
1250:
1170:Fundamental group
1095:and the Isabelle/
1039:natural deduction
973:BSD-style license
935:
934:
907:Carsten SchĂźrmann
865:SRI International
647:Leonardo de Moura
204:System comparison
155:
154:
147:
93:
92:
16:(Redirected from
2203:
2196:Proof assistants
2162:
2160:
2158:
2153:on 10 April 2022
2149:. Archived from
2074:
2067:
2063:
2060:
2054:
2022:
2021:
2014:
2005:
2003:
1993:
1967:
1940:
1932:
1919:
1917:
1911:. Archived from
1896:
1888:Barendregt, Henk
1874:
1873:
1871:
1870:
1855:
1849:
1848:
1846:
1845:
1830:
1824:
1823:
1821:
1809:
1803:
1802:
1800:
1799:
1784:
1778:
1777:
1775:
1774:
1743:
1725:
1719:
1718:
1716:
1715:
1700:
1694:
1693:
1691:
1666:
1654:
1648:
1647:
1637:
1627:
1603:
1597:
1596:
1588:
1582:
1581:
1579:
1577:
1567:"VS Code Lean 4"
1563:
1557:
1556:
1554:
1552:
1541:
1535:
1534:
1527:
1521:
1520:
1518:
1516:
1481:
1475:
1474:
1461:
1455:
1454:
1452:
1450:
1436:
1430:
1420:
1414:
1413:
1411:
1409:
1399:
1393:
1392:
1390:
1388:
1374:
1363:
1362:
1338:
1329:
1323:
1322:
1314:
1227:
1225:
1224:
1219:
1217:
1216:
1211:
1135:Proof assistant
1129:
283:J Strother Moore
254:Proof automation
218:
167:computer science
150:
143:
139:
136:
130:
125:this article by
116:inline citations
103:
102:
95:
88:
85:
79:
59:
51:
21:
2211:
2210:
2206:
2205:
2204:
2202:
2201:
2200:
2176:
2175:
2156:
2154:
2145:
2075:
2064:
2058:
2055:
2036:
2027:This article's
2023:
2019:
2012:
2001:
1996:
1990:
1970:
1964:
1943:
1930:
1924:Pfenning, Frank
1922:
1915:
1909:
1894:
1886:
1883:
1878:
1877:
1868:
1866:
1857:
1856:
1852:
1843:
1841:
1839:Quanta Magazine
1832:
1831:
1827:
1811:
1810:
1806:
1797:
1795:
1786:
1785:
1781:
1772:
1770:
1760:
1727:
1726:
1722:
1713:
1711:
1702:
1701:
1697:
1689:
1664:
1656:
1655:
1651:
1605:
1604:
1600:
1590:
1589:
1585:
1575:
1573:
1565:
1564:
1560:
1550:
1548:
1543:
1542:
1538:
1529:
1528:
1524:
1514:
1512:
1483:
1482:
1478:
1463:
1462:
1458:
1448:
1446:
1438:
1437:
1433:
1421:
1417:
1407:
1405:
1403:"The Agda Wiki"
1401:
1400:
1396:
1386:
1384:
1376:
1375:
1366:
1359:
1336:
1331:
1330:
1326:
1316:
1315:
1311:
1306:
1256:
1206:
1201:
1200:
1124:
1118:
1109:
1074:
1072:User interfaces
605:Makarius Wenzel
264:Code generation
244:Dependent types
216:
206:
175:proof assistant
151:
140:
134:
131:
121:Please help to
120:
104:
100:
89:
83:
80:
73:
60:
49:
42:
35:
28:
23:
22:
15:
12:
11:
5:
2209:
2207:
2199:
2198:
2193:
2188:
2178:
2177:
2174:
2173:
2164:
2143:
2138:
2133:
2128:
2123:
2117:
2116:
2112:
2111:
2106:
2101:
2095:
2088:"Introduction"
2085:
2077:
2076:
2031:external links
2026:
2024:
2017:
2011:
2010:External links
2008:
2007:
2006:
1994:
1988:
1968:
1962:
1941:
1920:
1918:on 2007-07-27.
1907:
1882:
1879:
1876:
1875:
1850:
1825:
1804:
1779:
1758:
1720:
1695:
1649:
1598:
1583:
1558:
1536:
1522:
1496:(2): 213â248.
1476:
1456:
1431:
1415:
1394:
1364:
1357:
1324:
1308:
1307:
1305:
1302:
1301:
1300:
1287:
1281:
1275:
1269:
1263:
1255:
1252:
1249:
1248:
1245:
1242:
1235:
1234:
1231:
1228:
1215:
1210:
1196:
1195:
1192:
1189:
1183:
1182:
1179:
1176:
1166:
1165:
1162:
1159:
1153:
1152:
1149:
1146:
1140:
1139:
1136:
1133:
1117:
1114:
1108:
1105:
1073:
1070:
1069:
1068:
1058:
1052:
1046:
1032:
1026:
1020:
1015:
1010:
1004:
998:
995:
994:
993:
986:
976:
948:
942:
933:
932:
929:
926:
923:
920:
917:
914:
909:
903:Frank Pfenning
900:
897:
891:
890:
887:
884:
881:
878:
875:
872:
867:
862:
859:
853:
852:
849:
846:
843:
840:
837:
834:
829:
824:
821:
815:
814:
812:
810:
808:
806:
804:
802:
800:
798:
796:
790:
789:
786:
783:
780:
777:
774:
771:
766:
761:
758:
752:
751:
749:
747:
745:
743:
741:
739:
734:
731:
728:
722:
721:
718:
715:
712:
709:
706:
703:
698:
688:
685:
679:
678:
675:
672:
669:
666:
663:
660:
654:
644:
641:
635:
634:
631:
628:
625:
622:
619:
616:
607:
586:
583:
577:
576:
573:
570:
567:
564:
561:
558:
553:
550:
547:
541:
540:
537:
534:
531:
528:
525:
522:
517:
514:
511:
505:
504:
501:
498:
495:
492:
489:
486:
481:
478:
475:
469:
468:
465:
462:
459:
456:
453:
450:
445:
436:
433:
427:
426:
423:
420:
417:
414:
411:
408:
403:
398:
395:
389:
388:
385:
382:
379:
376:
373:
370:
365:
362:
359:
353:
352:
349:
346:
343:
340:
337:
334:
329:
318:
315:
309:
308:
305:
302:
299:
296:
293:
290:
285:
276:
273:
267:
266:
261:
256:
251:
246:
241:
235:
234:
231:
228:
225:
224:Latest version
222:
205:
202:
153:
152:
107:
105:
98:
91:
90:
63:
61:
54:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
2208:
2197:
2194:
2192:
2189:
2187:
2184:
2183:
2181:
2172:
2168:
2165:
2152:
2148:
2144:
2142:
2139:
2137:
2134:
2132:
2129:
2127:
2124:
2122:
2119:
2118:
2114:
2113:
2110:
2107:
2105:
2102:
2099:
2096:
2093:
2089:
2086:
2084:
2081:
2080:
2073:
2070:
2062:
2059:December 2022
2052:
2048:
2047:inappropriate
2044:
2040:
2034:
2032:
2025:
2016:
2015:
2009:
2000:
1995:
1991:
1985:
1981:
1977:
1973:
1969:
1965:
1963:3-540-61064-2
1959:
1955:
1951:
1947:
1942:
1938:
1937:
1929:
1925:
1921:
1914:
1910:
1904:
1900:
1893:
1889:
1885:
1884:
1880:
1864:
1860:
1854:
1851:
1840:
1836:
1829:
1826:
1820:
1815:
1808:
1805:
1793:
1789:
1783:
1780:
1769:
1765:
1761:
1755:
1751:
1747:
1742:
1737:
1733:
1732:
1724:
1721:
1710:on 2016-11-19
1709:
1705:
1699:
1696:
1688:
1684:
1680:
1676:
1672:
1671:
1663:
1659:
1653:
1650:
1645:
1641:
1636:
1631:
1626:
1621:
1617:
1613:
1609:
1602:
1599:
1594:
1587:
1584:
1572:
1568:
1562:
1559:
1547:
1540:
1537:
1532:
1526:
1523:
1511:
1507:
1503:
1499:
1495:
1491:
1487:
1480:
1477:
1472:
1471:
1466:
1460:
1457:
1445:
1441:
1435:
1432:
1429:
1425:
1419:
1416:
1404:
1398:
1395:
1383:
1379:
1373:
1371:
1369:
1365:
1360:
1354:
1350:
1346:
1342:
1335:
1328:
1325:
1320:
1313:
1310:
1303:
1299:
1295:
1291:
1288:
1285:
1282:
1279:
1278:QED manifesto
1276:
1273:
1270:
1267:
1264:
1261:
1258:
1257:
1253:
1246:
1243:
1241:= 47,176,870
1240:
1237:
1236:
1232:
1229:
1213:
1198:
1197:
1193:
1190:
1188:
1185:
1184:
1180:
1177:
1175:
1171:
1168:
1167:
1163:
1160:
1158:
1155:
1154:
1150:
1147:
1145:
1142:
1141:
1130:
1127:
1123:
1115:
1113:
1106:
1104:
1102:
1098:
1094:
1090:
1085:
1083:
1079:
1071:
1066:
1062:
1059:
1056:
1053:
1050:
1047:
1044:
1040:
1036:
1033:
1030:
1027:
1024:
1021:
1019:
1016:
1014:
1011:
1008:
1005:
1002:
999:
996:
991:
987:
984:
980:
977:
974:
970:
966:
962:
959:
958:
956:
952:
949:
946:
943:
940:
937:
936:
930:
927:
924:
921:
918:
915:
913:
910:
908:
904:
901:
898:
896:
893:
892:
888:
885:
882:
879:
876:
873:
871:
868:
866:
863:
860:
858:
855:
854:
850:
847:
844:
841:
838:
835:
833:
830:
828:
825:
822:
820:
817:
816:
813:
811:
809:
807:
805:
803:
801:
799:
797:
795:
792:
791:
787:
784:
781:
778:
775:
772:
770:
767:
765:
762:
759:
757:
754:
753:
750:
748:
746:
744:
742:
740:
738:
735:
733:Norman Megill
732:
729:
727:
724:
723:
719:
716:
713:
710:
707:
704:
702:
699:
696:
692:
691:Randy Pollack
689:
686:
684:
681:
680:
676:
673:
670:
667:
664:
661:
658:
655:
652:
648:
645:
642:
640:
637:
636:
632:
629:
626:
623:
620:
617:
615:
611:
608:
606:
602:
598:
597:Tobias Nipkow
594:
590:
589:Larry Paulson
587:
584:
582:
579:
578:
574:
571:
568:
565:
562:
559:
557:
554:
551:
548:
546:
543:
542:
538:
535:
532:
529:
526:
523:
521:
518:
515:
512:
510:
507:
506:
502:
499:
496:
493:
490:
487:
485:
482:
480:John Harrison
479:
476:
474:
471:
470:
466:
463:
460:
457:
454:
451:
449:
446:
444:
440:
437:
434:
432:
429:
428:
424:
421:
418:
415:
412:
409:
407:
404:
402:
399:
396:
394:
391:
390:
386:
383:
380:
377:
374:
371:
369:
366:
364:Helmut Brandl
363:
360:
358:
355:
354:
350:
347:
344:
341:
338:
335:
333:
330:
327:
323:
319:
316:
314:
311:
310:
306:
303:
300:
297:
294:
291:
289:
286:
284:
280:
279:Matt Kaufmann
277:
274:
272:
269:
268:
265:
262:
260:
257:
255:
252:
250:
247:
245:
242:
240:
237:
236:
219:
215:
211:
203:
201:
199:
194:
192:
188:
184:
183:formal proofs
180:
176:
172:
168:
159:
149:
146:
138:
135:November 2018
128:
124:
118:
117:
111:
106:
97:
96:
87:
84:February 2024
77:
71:
67:
64:This article
62:
58:
53:
52:
47:
40:
33:
19:
2155:. Retrieved
2151:the original
2091:
2065:
2056:
2041:by removing
2028:
1979:
1945:
1934:
1913:the original
1898:
1867:. Retrieved
1865:. 2024-07-02
1862:
1853:
1842:. Retrieved
1838:
1828:
1807:
1796:. Retrieved
1794:. 2022-03-11
1791:
1782:
1771:. Retrieved
1730:
1723:
1712:. Retrieved
1708:the original
1698:
1674:
1668:
1652:
1615:
1611:
1601:
1586:
1574:. Retrieved
1570:
1561:
1549:. Retrieved
1539:
1525:
1513:. Retrieved
1493:
1489:
1479:
1468:
1459:
1447:. Retrieved
1443:
1434:
1418:
1406:. Retrieved
1397:
1385:. Retrieved
1381:
1340:
1327:
1312:
1125:
1110:
1086:
1075:
249:Small kernel
227:Developer(s)
195:
178:
174:
164:
141:
132:
113:
81:
65:
2157:15 February
1618:(1): 3â25.
1065:formulation
1041:style, and
990:Standard ML
912:Standard ML
870:Common Lisp
832:Common Lisp
769:Free Pascal
701:Standard ML
610:Standard ML
552:Edwin Brady
520:Standard ML
288:Common Lisp
127:introducing
2180:Categories
2115:Catalogues
1881:References
1869:2024-07-09
1844:2023-12-07
1819:2311.00007
1798:2024-02-09
1792:IFLScience
1773:2023-12-07
1714:2023-12-07
1635:2066/75958
1576:15 October
1551:2 November
1546:"Isabelle"
1515:22 January
1449:15 October
1428:1803.06547
1120:See also:
477:repository
435:repository
326:Gothenburg
208:See also:
110:references
2043:excessive
1741:1301.3443
979:HOL Light
965:Moscow ML
931:UnÂknown
889:UnÂknown
695:Edinburgh
593:Cambridge
473:HOL Light
357:Albatross
233:Features
187:interface
76:talk page
1974:(1998).
1687:archived
1660:(2008),
1644:14827467
1292:â is an
1254:See also
1132:Theorem
1001:Isabelle
971:. Has a
922:UnÂknown
848:UnÂknown
726:Metamath
581:Isabelle
569:UnÂknown
549:2 0.6.0.
384:UnÂknown
322:Chalmers
317:2.6.4.3
191:computer
2037:Please
2029:use of
1768:5661377
1683:2463991
1612:SÄdhanÄ
1510:3084322
1408:31 July
1387:31 July
1290:Prover9
1172:of the
969:Poly/ML
773:Partial
659:, Lean
643:v4.7.0
601:MĂźnchen
572:Partial
348:Partial
332:Haskell
295:Untyped
123:improve
1986:
1960:
1905:
1766:
1756:
1681:
1642:
1571:GitHub
1508:
1470:GitHub
1444:GitHub
1382:GitHub
1355:
1174:circle
1029:MINLOG
1023:Matita
985:based.
760:8.1.11
737:ANSI C
730:v0.198
603:) and
397:8.19.0
212:, and
112:, but
68:about
2002:(PDF)
1931:(PDF)
1916:(PDF)
1895:(PDF)
1814:arXiv
1764:S2CID
1736:arXiv
1690:(PDF)
1665:(PDF)
1640:S2CID
1506:S2CID
1424:arXiv
1337:(PDF)
1304:Notes
1247:2024
1239:BB(5)
1233:2023
1194:2022
1191:Lean
1181:2013
1164:2012
1151:2005
1138:Year
1097:Scala
1093:jEdit
1078:Emacs
1035:Mizar
983:OCaml
899:1.7.1
895:Twelf
819:NuPRL
794:Nqthm
756:Mizar
687:1.3.1
614:Scala
556:Idris
545:Idris
484:OCaml
443:INRIA
406:OCaml
401:INRIA
368:OCaml
2167:DMOZ
2159:2024
1984:ISBN
1958:ISBN
1903:ISBN
1754:ISBN
1578:2023
1553:2019
1517:2020
1451:2023
1410:2024
1389:2024
1353:ISBN
1296:for
1244:Coq
1230:Lean
1049:PhoX
1018:LEGO
1013:Lean
1007:Jape
967:and
961:HOL4
939:ACL2
905:and
851:Yes
683:LEGO
677:Yes
674:Yes
671:Yes
668:Yes
665:Yes
662:Yes
639:Lean
633:Yes
575:Yes
539:Yes
509:HOL4
467:Yes
441:and
425:Yes
361:0.4
324:and
313:Agda
281:and
271:ACL2
221:Name
173:, a
169:and
2090:in
2045:or
1950:doi
1746:doi
1630:hdl
1620:doi
1498:doi
1345:doi
1178:Coq
1161:Coq
1148:Coq
1089:Gtk
1061:TPS
945:Coq
919:Yes
916:Yes
883:Yes
877:Yes
874:Yes
861:6.0
857:PVS
845:Yes
842:Yes
839:Yes
836:Yes
788:No
776:Yes
720:No
711:Yes
708:Yes
705:Yes
657:C++
630:Yes
627:Yes
624:Yes
618:Yes
595:),
566:Yes
563:Yes
560:Yes
533:Yes
530:Yes
524:Yes
503:No
497:Yes
494:Yes
488:Yes
464:Yes
461:Yes
455:Yes
452:Yes
422:Yes
419:Yes
416:Yes
413:Yes
410:Yes
393:Coq
381:Yes
378:Yes
372:Yes
342:Yes
339:Yes
336:Yes
304:Yes
301:Yes
275:8.3
177:or
165:In
2182::
2169::
1956:.
1933:.
1926:.
1861:.
1837:.
1790:.
1762:.
1752:.
1744:.
1685:,
1679:MR
1675:55
1673:,
1667:,
1638:.
1628:.
1616:34
1614:.
1610:.
1569:.
1504:.
1494:11
1492:.
1488:.
1467:.
1442:.
1380:.
1367:^
1351:.
1339:.
1084:.
928:No
925:No
886:No
880:No
785:No
782:No
779:No
717:No
714:No
653:)
621:No
612:,
536:No
527:No
500:No
491:No
458:No
448:F*
431:F*
375:No
345:No
298:No
292:No
193:.
2161:.
2094:.
2072:)
2066:(
2061:)
2057:(
2053:.
2035:.
1992:.
1966:.
1952::
1872:.
1847:.
1822:.
1816::
1801:.
1776:.
1748::
1738::
1717:.
1646:.
1632::
1622::
1595:.
1580:.
1555:.
1519:.
1500::
1473:.
1453:.
1426::
1412:.
1391:.
1361:.
1347::
1321:.
1214:2
1209:F
1045:.
992:.
975:.
823:5
697:)
693:(
649:(
599:(
591:(
328:)
148:)
142:(
137:)
133:(
119:.
86:)
82:(
78:.
72:.
48:.
41:.
34:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
