Edithistory:Proof assistant
From EverybodyWiki Bios & Wiki
| oldid | date/time | username | edit summary |
|---|---|---|---|
| 1380223205 | 2026-10-14T14:25:13Z | Fgnievinski | Nominated for merging; see [[:Wikipedia:Articles for deletion/Proof assistant]]. |
| 1379082004 | 2026-10-07T21:01:21Z | Oneequalsequalsone | |
| 1376084104 | 2026-09-21T23:58:44Z | Myzhang1029 | /* System comparison */ Update Lean version and make them consistent without the leading v |
| 1375426941 | 2026-09-17T18:34:39Z | Jarble | editing a link |
| 1373892806 | 2026-09-08T15:47:56Z | EternallyOutbound | |
| 1370544564 | 2026-08-21T19:17:53Z | Jarble | added [[Template:Mathematical software]] |
| 1365446350 | 2026-07-22T13:19:20Z | 1234qwer1234qwer4 | /* System comparison */ consistent engvar |
| 1362554749 | 2026-07-04T19:13:38Z | Oklopfer | substitute per [[MOS:SECTIONANCHOR]] |
| 1356566535 | 2026-05-28T15:22:13Z | ~2026-31882-76 | /* See also */ |
| 1354245531 | 2026-05-15T05:30:43Z | MTardigradum | "strongly influence by" --> "strongly influenced by" |
| 1350774413 | 2026-04-23T23:30:09Z | Jon Daker | Remove Logic Theorist from the history section since this page is about ITPs not ATPs |
| 1350762768 | 2026-04-23T21:40:18Z | Jon Daker | Specifically mention Edinburgh LCF |
| 1350762444 | 2026-04-23T21:37:42Z | Jon Daker | Be more specific instead of "more recently" |
| 1350762192 | 2026-04-23T21:35:15Z | Jon Daker | Fill in the history section with ACL2, LCF, and Rocq |
| 1350759922 | 2026-04-23T21:16:45Z | Jon Daker | Undid revision [[Special:Diff/1350759874|1350759874]] by [[Special:Contributions/Jon Daker|Jon Daker]] ([[User talk:Jon Daker|talk]]) |
| 1350759874 | 2026-04-23T21:16:25Z | Jon Daker | Use em dash instead of |
| 1350723445 | 2026-04-23T16:19:41Z | Jon Daker | Update Rocq description, move to the right place in alphabetical order |
| 1350723183 | 2026-04-23T16:17:39Z | Jon Daker | Link to calculus of constructions |
| 1350563016 | 2026-04-22T16:56:20Z | Yonoteam | Clarified relationship between Isabelle and HOL |
| 1350561193 | 2026-04-22T16:43:20Z | Yonoteam | Updated |
| 1349425390 | 2026-04-17T07:46:15Z | Simxaraba | Don't see the issue here |
| 1349425337 | 2026-04-17T07:45:45Z | Simxaraba | /* Notes */ reflist |
| 1345739047 | 2026-03-27T21:56:03Z | Dbrusilo | Removed access-date parameter from cite book template. |
| 1342576033 | 2026-03-09T18:29:42Z | Jon Daker | Add Logic Theorist to history section |
| 1342397347 | 2026-03-08T19:13:51Z | ~2026-14851-63 | System comparison: add brief snippet describing Lean |
| 1340074736 | 2026-02-23T20:44:50Z | FaviFake | /* History */ [[H:M|merged]] content from [[Automated proof checking]] following a merge proposal. For the full discussion which led to the merge, please see the articles' talk pages. Please see the source page's history for [[WP:CWW|attribution]]. I didn't add additional content (just reorganised it), but the target section may need to be cleaned up. |
| 1339154208 | 2026-02-19T04:57:47Z | SchlurcherBot | Bot: http → https |
| 1336140701 | 2026-02-02T03:56:18Z | Komyyy | Leonard de Moura is now works at AWS |
| 1336140116 | 2026-02-02T03:51:47Z | Komyyy | /* System comparison */updated Lean's latest version |
| 1336083796 | 2026-02-01T21:39:40Z | Whisperjanes | Remove possible AI generation (possible hallucinations with strange or vague phrasing e.g. "LCF family") - per user's recent editing history |
| 1335855705 | 2026-01-31T16:23:30Z | Nuclear Catapult | Updating latest version of Agda from 2.6.4.3 to 2.8.0 |
| 1333071088 | 2026-01-15T15:04:59Z | Lfstevens | Filled in 0 bare reference(s) with reFill 2 |
| 1332875215 | 2026-01-14T09:42:00Z | Wojciech Buzderewicz | Expanded history section; added explanation of proof checking and trusted kernel; added inline citations from secondary sources |
| 1331699524 | 2026-01-07T18:49:38Z | Jarble | link to talk page section |
| 1328204405 | 2025-12-18T14:08:29Z | GhostInTheMachine | Changing [[Wikipedia:Short description|short description]] from "interactive software theorem prover" to "Interactive theorem prover software" |
| 1328193739 | 2025-12-18T12:14:26Z | MichaelMaggs | Changing [[Wikipedia:Short description|short description]] from "Software tool to assist with the development of formal proofs by human–machine collaboration" to "interactive software theorem prover" |
| 1326801647 | 2025-12-10T23:44:09Z | Explicit | Removed deleted item from hatnote. |
| 1325800003 | 2025-12-05T06:41:05Z | ALittleClass | /* History */ section needs expansion |
| 1324926358 | 2025-11-30T07:40:04Z | ALittleClass | starting history section |
| 1319565958 | 2025-10-30T15:57:35Z | LuniZunie | Reverted edits by [[Special:Contributions/38.52.122.233|38.52.122.233]] ([[User talk:38.52.122.233|talk]]): vandalism ([[WP:AntiVandal|AV]]) |
| 1319565690 | 2025-10-30T15:56:15Z | 38.52.122.233 | |
| 1317317522 | 2025-10-17T14:05:10Z | PoCc001 | /* {{anchor|Comparison}}System comparison */ |
| 1317317454 | 2025-10-17T14:04:44Z | PoCc001 | /* {{anchor|Comparison}}System comparison */ Isabelle2025 is available |
| 1312668865 | 2025-09-21T23:59:51Z | 37.75.87.139 | /* Formalization extent */ Update to most recent stats |
| 1312668207 | 2025-09-21T23:53:25Z | 37.75.87.139 | Update Lean to v4.23.0 |
| 1311879597 | 2025-09-17T12:08:30Z | Maxbmn | Coq -> Rocq |
| 1311319590 | 2025-09-14T18:06:31Z | Shhhnotsoloud | Amend hatnote ([[WP:HATNOTE]]) |
| 1308748391 | 2025-08-31T07:43:05Z | Jerryobject | /* {{anchor|Comparison}}System comparison */ Layout shrink: [[newline]] add. De[[WP:LINK]] [[WP:RED]] [[WP:REDNOT]]s. Alphabetize entry. Small [[WP:COPYEDIT]] [[WP:EoS]] [[WP:REFPUNCT]]uation. [[MOS:COMMENT]] add. |
| 1308535416 | 2025-08-30T01:38:49Z | Jerryobject | /* {{anchor|Comparison}}System comparison */ Cut needless [[whitespace character]]s (spaces, [[carriage return]]s) to standardize, aid work via small screens. [[WP:REF]]erence [[WP:CIT]]ation parameters: add, fill, author > last + first, reorder, update-standardize. [[WP:LINK]]s: update-standardizes, needless-[[WP:PIPE]]s > [[WP:NOPIPE]]s, [[WP:RED]] [[WP:REDNOT]] delink. Small [[WP:COPYEDIT]]s [[WP:EoS]] [[WP:TERSE]]. [[MOS:FIRSTABBR]]eviation define-clarify before parenthetic [[WP:ABBR]]. |
| 1308050840 | 2025-08-27T06:24:57Z | Citation bot | Removed URL that duplicated identifier. Removed access-date with no URL. | [[:en:WP:UCB|Use this bot]]. [[:en:WP:DBUG|Report bugs]]. | Suggested by Headbomb | Linked from Wikipedia:WikiProject_Academic_Journals/Journals_cited_by_Wikipedia/Sandbox | #UCB_webform_linked 155/967 |
| 1291974133 | 2025-05-24T13:56:56Z | OAbot | [[Wikipedia:OABOT|Open access bot]]: url-access updated in citation with #oabot. |
| 1283961142 | 2025-04-04T18:58:09Z | Kaffet i halsen | University of Gothenburg + sp (via [[WP:JWB]]) |
| 1283028835 | 2025-03-30T00:41:54Z | Citation bot | Altered title. | [[:en:WP:UCB|Use this bot]]. [[:en:WP:DBUG|Report bugs]]. | Suggested by Ringo62 | [[Category:Proof assistants]] | #UCB_Category 4/28 |
| 1282971525 | 2025-03-29T17:56:46Z | Ringo62 | ce |
| 1281094570 | 2025-03-18T07:34:05Z | Cedar101 | /* {{anchor|Comparison}}System comparison */ <br/> |
| 1281074396 | 2025-03-18T03:30:07Z | Jfire | Reverted edits by [[Special:Contribs/103.136.206.213|103.136.206.213]] ([[User talk:103.136.206.213|talk]]) to last version by Valvino |
| 1281074003 | 2025-03-18T03:27:03Z | 103.136.206.213 | |
| 1281073898 | 2025-03-18T03:25:54Z | 103.136.206.213 | |
| 1280688638 | 2025-03-15T22:12:49Z | Valvino | Coq -> Rocq |
| 1250500502 | 2024-10-10T20:02:38Z | 81.172.153.200 | /* {{anchor|Comparison}}System comparison */ |
| 1244534621 | 2024-09-07T17:51:48Z | Oneequalsequalsone | /* System comparison */ obviously its not affiliated with Lego |
| 1238127126 | 2024-08-02T07:39:12Z | Lfstevens | Filled in 1 bare reference(s) with reFill 2 |
| 1237761872 | 2024-07-31T10:41:30Z | Andrewchawk | I added some citation stuff for Agda. |
| 1233588940 | 2024-07-09T21:52:45Z | Tajoshu | /* Notable formalized proofs */ added BB(5) proof (Busy beaver) |
| 1233085231 | 2024-07-07T05:45:25Z | Sam Hnri | |
| 1226931114 | 2024-06-02T16:56:46Z | 91.200.238.244 | Update versions of Mizar and Isabelle |
| 1226045445 | 2024-05-28T07:15:53Z | WikiCleanerBot | v2.05b - [[User:WikiCleanerBot#T20|Bot T20 CW#61]] - Fix errors for [[WP:WCW|CW project]] (Reference before punctuation) |
| 1225677676 | 2024-05-26T01:01:44Z | 95.25.206.108 | |
| 1221680865 | 2024-05-01T10:45:43Z | 145.109.25.53 | /* System comparison */ Update the latest version of Lean. |
| 1211213908 | 2024-03-01T11:52:16Z | Citation bot | Alter: title, template type. Add: eprint, class, date. Removed proxy/dead URL that duplicated identifier. Removed parameters. Some additions/deletions were parameter name changes. | [[:en:WP:UCB|Use this bot]]. [[:en:WP:DBUG|Report bugs]]. | Suggested by Abductive | [[Category:Articles to be expanded from February 2024]] | #UCB_Category 770/944 |
| 1211055191 | 2024-02-29T16:36:33Z | AnomieBOT | Dating maintenance tags: {{Missing information}} |
| 1211052302 | 2024-02-29T16:16:28Z | Jarble | see the talk page discussion: [[automated proof checking]] isn't mentioned in the article. |
| 1207589343 | 2024-02-15T05:46:57Z | 182.233.91.64 | /* External links */ Replace [[Frank Pfenning]] with Frank Pfenning (for avoiding duplicated [[Wikilinks]]). |
| 1207585348 | 2024-02-15T05:31:00Z | 182.233.91.64 | /* External links */ Complement the dead link “Specific Logical Frameworks and Implementations” with its [[Wayback Machine]] archive [[URL]] and its author [[Frank Pfenning]]. |
| 1205307806 | 2024-02-09T10:23:34Z | Rob235711 | /* Notable formalized proofs */ Added Erdős-Graham problem to notable proofs table. |
| 1203795748 | 2024-02-05T16:20:12Z | Durbatuluk1701 | Updating latest Coq version |
| 1199021347 | 2024-01-25T17:47:49Z | Citation bot | Altered title. Added chapter. | [[:en:WP:UCB|Use this bot]]. [[:en:WP:DBUG|Report bugs]]. | Suggested by Abductive | [[Category:Automated theorem proving]] | #UCB_Category 38/39 |
| 1198036105 | 2024-01-22T20:32:00Z | SunshineAllNight | /* Notable formalized proofs */clarified formalized polynomial freiman-ruza result is over finite field of characteristic 2 |
| 1193840013 | 2024-01-05T22:53:17Z | OAbot | [[Wikipedia:OABOT|Open access bot]]: hdl updated in citation with #oabot. |
| 1189340865 | 2023-12-11T06:32:03Z | Citation bot | Alter: url, template type, title. URLs might have been anonymized. Add: s2cid, isbn, arxiv, pages, date, archive-date, archive-url, authors 1-2. Removed parameters. | [[:en:WP:UCB|Use this bot]]. [[:en:WP:DBUG|Report bugs]]. | Suggested by Abductive | [[Category:Proof assistants]] | #UCB_Category 26/28 |
| 1188818377 | 2023-12-07T21:59:19Z | Siddharthist | /* Notable formalized proofs */ Add four-color theorem |
| 1188817349 | 2023-12-07T21:50:17Z | Siddharthist | /* Notable formalized proofs */ Fundamental group of the circle in HoTT |
| 1188816813 | 2023-12-07T21:46:09Z | Siddharthist | /* Notable formalized proofs */ See also |
| 1188816749 | 2023-12-07T21:45:41Z | Siddharthist | List of theorems proved |
| 1185619274 | 2023-11-17T22:57:42Z | Countercheck | added a See Also |
| 1185618050 | 2023-11-17T22:48:53Z | Countercheck | adjusted picture size using upright |
| 1185617840 | 2023-11-17T22:47:15Z | Citation bot | Add: journal, website, title. Changed bare reference to CS1/2. Removed parameters. Some additions/deletions were parameter name changes. | [[:en:WP:UCB|Use this bot]]. [[:en:WP:DBUG|Report bugs]]. | Suggested by Countercheck | #UCB_webform |
| 1185617477 | 2023-11-17T22:44:40Z | Countercheck | copyedit |
| 1184811884 | 2023-11-12T19:54:00Z | ElliAWB | Disambiguating links to [[Coq]] (link changed to [[Coq (software)]]; link changed to [[Coq (software)]]) using [[User:Qwertyytrewqqwerty/DisamAssist|DisamAssist]]. |
| 1180296464 | 2023-10-15T18:53:59Z | RedrickSchu | Updated Lean section to include official latest release and pre-release /* {{anchor|Comparison}}System comparison */ |
| 1180294968 | 2023-10-15T18:43:31Z | RedrickSchu | Fixed source for Lean 4 in /* User interfaces */ |
| 1180293979 | 2023-10-15T18:36:45Z | RedrickSchu | Added info on Lean 4 user interface |
| 1179782290 | 2023-10-12T11:53:57Z | Tea2min | Undid revision 1179775841 by [[Special:Contributions/Skoobadive100|Skoobadive100]] ([[User talk:Skoobadive100|talk]]): ? |
| 1179775841 | 2023-10-12T10:42:14Z | Skoobadive100 | |
| 1179132860 | 2023-10-08T03:20:18Z | Amakuha | |
| 1179132685 | 2023-10-08T03:17:55Z | Amakuha | /* Formalization extent */ added a secondary source quoting Wiedijk |
| 1177529969 | 2023-09-27T23:56:03Z | Amakuha | updated versions of Lean |
| 1177529678 | 2023-09-27T23:52:39Z | Amakuha | Lean 4 is implemented in itself |
| 1177522502 | 2023-09-27T22:56:19Z | Amakuha | |
| 1177317698 | 2023-09-27T04:35:30Z | Amakuha | /* Formalization extent */ new section |
| 1177291804 | 2023-09-27T02:12:37Z | Citation bot | Removed parameters. | [[:en:WP:UCB|Use this bot]]. [[:en:WP:DBUG|Report bugs]]. | #UCB_CommandLine |
| 1173861456 | 2023-09-04T21:34:08Z | Caleb Stanford | two important omissions |
| 1168705405 | 2023-08-04T13:28:51Z | Achmad Rachmani | URL error |
| 1168688615 | 2023-08-04T10:35:50Z | Skoobadive100 | |
| 1165710479 | 2023-07-16T23:07:36Z | 138.112.24.76 | Adding source name |
| 1165710209 | 2023-07-16T23:04:48Z | 138.112.24.76 | Adding most recent important effort |
| 1155998717 | 2023-05-20T18:55:33Z | Maxeto0910 | no sentence |
| 1149866572 | 2023-04-14T22:56:31Z | Julian Mendez | /* {{anchor|Comparison}}System comparison */ Updated version numbers |
| 1147040581 | 2023-03-28T13:55:31Z | Goens | /* {{anchor|Comparison}}System comparison */ Fill unknown value (Lean has a compiler and does support code generation) |
| 1146159930 | 2023-03-23T03:32:37Z | Minorax | trim |
| 1136343209 | 2023-01-29T22:08:57Z | OAbot | [[Wikipedia:OABOT|Open access bot]]: doi added to citation with #oabot. |
| 1127416295 | 2022-12-14T15:51:15Z | AnomieBOT | Dating maintenance tags: {{External links}} |
| 1127413542 | 2022-12-14T15:30:25Z | Skyerise | cleanup up external links in article body |
| 1127411846 | 2022-12-14T15:19:40Z | Skyerise | /* See also */ sort and annotate |
| 1127411448 | 2022-12-14T15:17:13Z | Skyerise | fix typo |
| 1127411390 | 2022-12-14T15:16:55Z | Skyerise | external links in article body... |
| 1109289390 | 2022-09-09T01:46:31Z | RDBrown | /* References */ →Cite book, journal | Alter: chapter-url, doi. URLs might have been anonymized. Add: s2cid, archive-date, archive-url. Removed parameters. | [[WP:UCB|Use this tool]]. [[WP:DBUG|Report bugs]]. | #UCB_Gadget |
| 1096111349 | 2022-07-02T11:04:25Z | Pochinha | Update latest Coq version |
| 1095913902 | 2022-07-01T05:08:37Z | 69.181.72.43 | /* System comparison */Wording |
| 1082224978 | 2022-04-12T00:43:54Z | TeraSibune | /* System comparison */ |
| 1071442179 | 2022-02-12T17:02:34Z | JulianBerman | Add version number for the more commonly-used version of Lean (the community fork) as well as the upcoming Lean 4 version. |
| 1071106729 | 2022-02-10T22:12:35Z | Qwerfjkl (bot) | Capitalising short description "software tool to assist with the development of formal proofs by human-machine collaboration" per [[WP:SDFORMAT]] (via [[de:Benutzer:Schnark/js/bandersnatch|Bandersnatch]]) |
| 1057998399 | 2021-11-30T21:41:31Z | MaxEnt | for hat formal verification |
| 1048855269 | 2021-10-08T11:04:23Z | Julian Mendez | /* {{anchor|Comparison}}System comparison */ |
| 1029655142 | 2021-06-21T07:56:13Z | Lfstevens | /* Comparison of systems */ |
| 1028743260 | 2021-06-15T19:05:17Z | 138.246.3.8 | /* {{anchor|Comparison}}Comparison of systems */ |
| 1027610008 | 2021-06-08T23:00:04Z | 73.241.189.191 | Update ACL2 version |
| 1026953856 | 2021-06-05T05:52:35Z | Tea2min | Per [[MOS:PIPEDLINK]], prefer redirects over piped links. |
| 1026919427 | 2021-06-05T00:34:09Z | 170.199.25.231 | link to standard ml implementations |
| 1025558040 | 2021-05-28T06:48:44Z | 41.13.68.209 | #suggestededit-add 1.0 |
| 1017537690 | 2021-04-13T10:11:19Z | Automated.Bee | /* {{anchor|Comparison}}Comparison of systems */ Update Idris info |
| 996162405 | 2020-12-24T22:05:29Z | CharlesC | /* Comparison of systems */ Added links |
| 995972953 | 2020-12-23T21:22:48Z | Monkbot | [[User:Monkbot/task 18|Task 18 (cosmetic)]]: eval 4 templates: del empty params (6×); hyphenate params (2×); del |url-status= (1×); |
| 994128958 | 2020-12-14T05:51:20Z | Citation bot | Add: title. | You can [[WP:UCB|use this bot]] yourself. [[WP:DBUG|Report bugs here]]. | Suggested by Headbomb | via #UCB_toolbar |
| 994128804 | 2020-12-14T05:49:58Z | Headbomb | ce |
| 994128739 | 2020-12-14T05:49:25Z | Citation bot | Add: s2cid, isbn, doi, series. Upgrade ISBN10 to ISBN13. | You can [[WP:UCB|use this bot]] yourself. [[WP:DBUG|Report bugs here]]. | Suggested by Headbomb | via #UCB_toolbar |
| 992763909 | 2020-12-06T23:44:00Z | Lennart97 | Disambiguated: [[Haskell]] → [[Haskell (programming language)]] |
| 984938412 | 2020-10-23T00:21:35Z | 31.205.91.171 | Add Idris to comparison |
| 975430916 | 2020-08-28T13:28:23Z | Hat shelf | Latest version of HOL4 is now Kananaskis-13: https://hol-theorem-prover.org/kananaskis-13.release.html |
| 971938507 | 2020-08-09T05:38:29Z | 2600:1700:2F70:8A0:5C70:AD07:678A:6AAC | /* User interfaces */added “a” |
| 968531233 | 2020-07-19T23:31:49Z | Bender the Bot | HTTP → HTTPS for [[Radboud University]] computer science department, replaced: http://www.cs.ru.nl/ → https://www.cs.ru.nl/ (3) |
| 964127328 | 2020-06-23T19:04:27Z | Pseudosalacia | /* Comparison of systems */ Update latest version of Isabelle |
| 960018440 | 2020-05-31T18:38:42Z | Bender235 | /* {{anchor|Comparison}}Comparison of systems */Replaced [[arXiv]] PDF link with more mobile-friendly abstract link, replaced: https://arxiv.org/pdf/ → https://arxiv.org/abs/ |
| 956197466 | 2020-05-12T01:24:32Z | InternetArchiveBot | Rescuing 1 sources and tagging 0 as dead.) #IABot (v2.0 |
| 938294741 | 2020-01-30T08:31:35Z | Tambora1815 | /* {{anchor|Comparison}}Comparison of systems */ Coq version 8.11.0 (28 January 2020): https://coq.inria.fr/news/coq-8-11-0-is-out.html |
| 937043350 | 2020-01-22T16:13:42Z | Vkuncak | /* {{anchor|Comparison}}Comparison of systems */ |
| 937042840 | 2020-01-22T16:09:23Z | Vkuncak | /* {{anchor|Comparison}}Comparison of systems */ |
| 937042630 | 2020-01-22T16:07:56Z | Vkuncak | /* {{anchor|Comparison}}Comparison of systems */ Added IMPS and its citation |
| 936926000 | 2020-01-21T21:29:49Z | Mdnahas | Replaced external link with link to new Lean (proof assistant) page |
| 930553246 | 2019-12-13T07:51:09Z | Tambora1815 | /* {{anchor|Comparison}}Comparison of systems */ Coq version 8.10.2 (29 November 2019): https://coq.inria.fr/news/coq-8-10-2-is-out.html |
| 927101007 | 2019-11-20T09:49:15Z | 130.190.104.213 | |
| 927097138 | 2019-11-20T09:12:44Z | Widefox | /* {{anchor|Comparison}}Comparison of systems */ simplify link |
| 924222726 | 2019-11-02T15:34:39Z | Vkuncak | /* User interface */ added vs code |
| 920471250 | 2019-10-10T00:39:26Z | Adyavanapalli | Previous link linked to the wrong page. |
| 920470983 | 2019-10-10T00:36:14Z | Adyavanapalli | Added latest version of the Lean proof assistant, along with a citation of said fact. |
| 919394282 | 2019-10-03T14:19:01Z | 211.106.108.14 | /* {{anchor|Comparison}}Comparison of systems */ |
| 916260144 | 2019-09-17T23:22:39Z | Jarble | linking |
| 914124652 | 2019-09-05T10:23:39Z | 128.243.2.33 | /* See also */ Add link. |
| 913090876 | 2019-08-29T20:32:44Z | Bender the Bot | HTTP → HTTPS for Carnegie Mellon CS, replaced: http://www.cs.cmu.edu/ → https://www.cs.cmu.edu/ (3) |
| 910488251 | 2019-08-12T12:26:53Z | 86.91.6.10 | /* Comparison of systems */ Updated Agda version |
| 907537245 | 2019-07-23T15:40:02Z | Positive failure | Update Isabelle version |
| 906188552 | 2019-07-14T06:52:52Z | Graeme Bartlett | clean up |
| 905933792 | 2019-07-12T13:10:05Z | 185.24.187.196 | /* See also */ |
| 902586384 | 2019-06-19T20:52:53Z | Ysangkok | /* {{anchor|Comparison}}Comparison of systems */ correct search string for f* |
| 902586183 | 2019-06-19T20:51:12Z | Ysangkok | /* {{anchor|Comparison}}Comparison of systems */ f* can do proofs by reflection |
| 898204388 | 2019-05-22T02:15:09Z | 50.196.138.183 | Update latest version of ACL2. |
| 894849910 | 2019-04-30T12:25:24Z | LambdaTotoro | /* Comparison of systems */ (m) improved link |
| 893749363 | 2019-04-23T10:23:15Z | 79.107.104.246 | WP:HNP |
| 892986765 | 2019-04-18T05:51:24Z | MichaelKohlhase | adding a reference to the theorem prover museum which has the sources of many of the systems. |
| 888834442 | 2019-03-21T18:29:52Z | 129.2.180.121 | /* {{anchor|Comparison}}Comparison of systems */ |
| 871769316 | 2018-12-03T09:04:11Z | Logiker~enwiki | Makarius Wenzel is no longer at Paris Sud (personal acquaintance/check out https://sketis.net/impressum-2) |
| 870081264 | 2018-11-22T07:05:34Z | Cedar101 | /* {{anchor|Comparison}}Comparison of systems */ {{not yet}} |
| 868877938 | 2018-11-15T01:00:21Z | AdamSobieski | |
| 868223892 | 2018-11-10T20:37:01Z | AnomieBOT | Dating maintenance tags: {{Inline}} |
| 868221402 | 2018-11-10T20:16:52Z | Boleyn | +inline tag |
| 861670274 | 2018-09-29T03:53:51Z | Jarble | adding links to references using [[Google Scholar]] |
| 861537638 | 2018-09-28T04:43:27Z | 150.203.114.201 | Update latest version for HOL4, see https://github.com/HOL-Theorem-Prover/HOL/releases |
| 859211723 | 2018-09-12T14:01:25Z | 86.29.206.96 | Removed "see also" entry that redirects back here |
| 856739789 | 2018-08-27T07:17:20Z | Smk65536 | bump isabelle version |
| 847007073 | 2018-06-22T08:05:03Z | 2001:660:4701:6001:2870:3DC:EDC0:2998 | /* {{anchor|Comparison}}Comparison of systems */ |
| 825273170 | 2018-02-12T13:18:56Z | 87.69.114.251 | /* {{anchor|Comparison}}Comparison of systems */ move Lean to place |
| 821607968 | 2018-01-21T14:49:05Z | 129.45.113.64 | /* {{anchor|Comparison}}Comparison of systems */ |
| 812071841 | 2017-11-25T20:54:05Z | 2001:4898:80E8:B:0:0:0:7B4 | |
| 800662925 | 2017-09-14T22:52:10Z | Helptry | /* External links: add list of tools */ |
| 798015972 | 2017-08-30T13:46:24Z | 201.97.61.132 | |
| 793657556 | 2017-08-03T04:33:30Z | Arto B | /* {{anchor|Comparison}}Comparison of systems */ Corrected capitalization. |
| 793418315 | 2017-08-01T16:38:02Z | 139.19.176.68 | The newest Coq version is 8.6.1 |
| 783090638 | 2017-05-31T02:20:55Z | Carstensen | /* {{anchor|Comparison}}Comparison of systems */ |
| 771947439 | 2017-03-24T12:36:17Z | Omnipaedista | see MOS:SECTIONORDER |
| 749419167 | 2016-11-14T06:07:33Z | 152.208.62.31 | /* {{anchor|Comparison}}Comparison of systems */ |
| 749418679 | 2016-11-14T06:03:11Z | 152.208.62.31 | /* {{anchor|Comparison}}Comparison of systems */ |
| 747488683 | 2016-11-02T17:36:28Z | Helmut.brandl | Added Albatross to the list |
| 747119073 | 2016-10-31T15:18:46Z | Positive failure | The latest version of Isabelle is 2016 - https://isabelle.in.tum.de |
| 741347471 | 2016-09-26T22:51:59Z | Clarityfiend | /* {{anchor|Comparison}}Comparison of systems */ bad link: redirects to pun generator |
| 739019790 | 2016-09-12T09:31:59Z | 116.8.123.241 | /* {{anchor|Comparison}}Comparison of systems */ |
| 730959919 | 2016-07-21T23:50:13Z | Hritcu | /* {{anchor|Comparison}}Comparison of systems */ |
| 730959873 | 2016-07-21T23:49:35Z | Hritcu | /* {{anchor|Comparison}}Comparison of systems */ |
| 730959727 | 2016-07-21T23:47:34Z | Hritcu | /* {{anchor|Comparison}}Comparison of systems */ Coloring Lean the right way |
| 730959589 | 2016-07-21T23:45:53Z | Hritcu | Started adding Lean to the list |
| 720496904 | 2016-05-16T07:05:36Z | HongxuChen | /* {{anchor|Comparison}}Comparison of systems */ |
| 714061782 | 2016-04-07T11:27:05Z | 2A02:2C40:100:A001:DE73:6FA2:A9E2:146C | /* {{anchor|Comparison}}Comparison of systems */ |
| 703261082 | 2016-02-04T13:13:34Z | Ruud Koot | /* References */ * [[Henk Barendregt]] and [[Herman Geuvers]] (2001). [http://www.ncc.up.pt/~nam/aulas/0506/t_coq/barendregt01proofassistants.pdf "Proof-assistants using Dependent Type Systems"]. In ''Handbook of Automated Reasoning''. |
| 702821595 | 2016-02-01T21:29:28Z | Hritcu | /* {{anchor|Comparison}}Comparison of systems */ Bumped F* version |
| 692830446 | 2015-11-28T16:50:39Z | Matěj Grabovský | /* See also */ capitalisation |
| 686147559 | 2015-10-17T09:25:13Z | Smk65536 | |
| 686025309 | 2015-10-16T14:15:24Z | Jiegec | /* Comparison of systems */ Update ACL2 Agda version |
| 685523881 | 2015-10-13T09:56:57Z | Hritcu | /* {{anchor|Comparison}}Comparison of systems */ New F* version |
| 680955886 | 2015-09-14T08:13:23Z | Hritcu | /* {{anchor|Comparison}}Comparison of systems */ Bumped F* version |
| 679950211 | 2015-09-07T20:10:26Z | 87.63.196.30 | /* {{anchor|Comparison}}Comparison of systems */ Update Agda devs |
| 677546053 | 2015-08-24T00:35:46Z | Hritcu | /* {{anchor|Comparison}}Comparison of systems */ made link more direct |
| 677545944 | 2015-08-24T00:34:44Z | Hritcu | Added F* to the comparison table |
| 677545500 | 2015-08-24T00:30:22Z | Hritcu | /* {{anchor|Comparison}}Comparison of systems */ |
| 665730972 | 2015-06-06T08:22:35Z | Adavidb | Disambiguate [[Code generation]] to [[Code generation (compiler)]] using [[:en:Wikipedia:Tools/Navigation_popups|popups]]; formatting: 14x nbsp-dash (using [[User:Cameltrader#Advisor.js|Advisor.js]]) |
| 655156155 | 2015-04-06T08:01:54Z | Jarble | fixing a [[WP:Broken section anchor]] |
| 634202698 | 2014-11-17T09:55:11Z | 86.129.175.193 | Bump Agda version |
| 632805903 | 2014-11-07T08:57:34Z | Smk65536 | removed redundancy and better description |
| 618184840 | 2014-07-23T22:27:06Z | Monkbot | /* Comparison of systems */Task 5: Fix [[Help:CS1_errors#deprecated_params|CS1 deprecated coauthor parameter errors]] |
| 614345548 | 2014-06-25T10:09:44Z | 131.174.138.214 | /* Comparison of systems */ Add Mizar |
| 602268120 | 2014-04-01T14:13:33Z | Qwertyus | +hatnote |
| 585905951 | 2013-12-13T14:05:38Z | 2001:62A:4:2F00:221:86FF:FE1C:2AB7 | changed the link of Isabelle, such that no redirect is necessary |
| 551915047 | 2013-04-24T05:50:54Z | Addbot | [[User:Addbot|Bot:]] Migrating 2 interwiki links, now provided by [[Wikipedia:Wikidata|Wikidata]] on [[d:q11387554]] |
| 550699003 | 2013-04-16T20:35:17Z | Xrchz | /* Comparison of systems */ add HOL4 to table, and tweak info about it below |
| 546060289 | 2013-03-21T19:23:07Z | Khazar2 | /* Comparison of systems */clean up, [[WP:AWB/T|typos fixed]]: best-known → best known using [[Project:AWB|AWB]] (8853) |
| 545190258 | 2013-03-18T09:33:38Z | 72.14.228.1 | Replacing the word "man" with "human" |
| 541900557 | 2013-03-03T15:30:57Z | 90.2.244.81 | Isabelle is not really another "HOL", but an independent member of the greater LCF family (like Coq) |
| 541899929 | 2013-03-03T15:24:51Z | 90.2.244.81 | more on user interfaces |
| 541899407 | 2013-03-03T15:20:05Z | 90.2.244.81 | more specific information on LEGO, although that is a historic system and hard to check now |
| 541899182 | 2013-03-03T15:17:57Z | 90.2.244.81 | updated "Code Generation" column to the best of my knowledge |
| 541898333 | 2013-03-03T15:09:56Z | 90.2.244.81 | "code generation" is the more general term, which covers both the way of Coq and Isabelle/HOL, and others |
| 541898134 | 2013-03-03T15:07:33Z | 90.2.244.81 | updated to Isabelle2013 -- the system is just called "Isabelle", while "Isabelle/HOL" is its main application |
| 540110821 | 2013-02-24T18:26:21Z | RjwilmsiBot | /* Comparison of systems */fixing page range dashes using [[Project:AWB|AWB]] |
| 522844087 | 2012-11-13T16:29:09Z | Ruud Koot | /* References */ * [[Robert L. Constable]] (1998). "Types in computer science, philosophy and logic". In ''Handbook of Proof Theory''. * Frank Pfenning (1999). "Logical frameworks". In ''Handbook of Automated Reasoning''. |
| 514411578 | 2012-09-24T23:37:54Z | Ruud Koot | {{confused|Interactive proof system}} |
| 514215450 | 2012-09-23T20:44:15Z | Jesin | /* Comparison of systems */ |
| 513789455 | 2012-09-20T23:00:34Z | 129.10.117.224 | |
| 513788863 | 2012-09-20T22:57:08Z | 129.10.117.224 | |
| 513788536 | 2012-09-20T22:55:08Z | 129.10.117.224 | /* Comparison of systems */ |
| 513781390 | 2012-09-20T22:09:40Z | MisterCarl | /* Comparison of systems */ Cleaning up the chart: fairer evaluation of ACL2, changed "partial" where meaning was unclear, added missing "unknown"s |
| 507697153 | 2012-08-16T15:17:01Z | 2001:67C:1220:80C:21C:C0FF:FE6C:6330 | /* Comparison of systems */ |
| 506252698 | 2012-08-07T16:52:10Z | Michael Hardy | multiple punctuation corrections required by [[WP:MOS]]; deleted "stub" tags |
| 505309350 | 2012-08-01T19:28:49Z | Ken Gallager | disambig Haskell |
| 503670571 | 2012-07-22T23:23:51Z | Ruud Koot | /* See also */ rm redirect |
| 503670490 | 2012-07-22T23:23:15Z | Ruud Koot | /* See also */ [[Automated proof checking]] |
| 503669665 | 2012-07-22T23:17:55Z | Ruud Koot | move list of systems back below table |
| 503163541 | 2012-07-19T19:16:24Z | 128.36.158.67 | /* Comparison table */ |
| 499608423 | 2012-06-27T14:22:42Z | 130.238.11.137 | /* Comparison table */ |
| 499608353 | 2012-06-27T14:22:13Z | 130.238.11.137 | /* Comparison table */ |
| 495488593 | 2012-06-01T17:17:56Z | Crisperdue | /* Comparison table */ |
| 495488540 | 2012-06-01T17:17:30Z | Crisperdue | /* Comparison table */ |
| 495488422 | 2012-06-01T17:16:40Z | Crisperdue | Add HOL Light to comparison table |
| 495487750 | 2012-06-01T17:12:31Z | Crisperdue | Put system listings first and title as such |
| 487648840 | 2012-04-16T11:13:13Z | 79.119.8.1 | /* See also */ |
| 481123463 | 2012-03-10T06:25:39Z | 209.133.117.5 | nuprl |
| 467027513 | 2011-12-21T14:26:18Z | CLeJ37 | Isabelle supports program extraction |
| 467026982 | 2011-12-21T14:20:47Z | CLeJ37 | update last version for Isabelle |
| 466922909 | 2011-12-20T21:54:34Z | 88.68.17.62 | /* Comparison */ Corrected Agda version |
| 466922804 | 2011-12-20T21:53:48Z | 88.68.17.62 | /* Comparison */ Update to newest Agda version, which also supports proofs by reflection to some extent |
| 464310890 | 2011-12-06T01:04:34Z | Ruud Koot | /* References */ * Freek Wiedijk. "[http://www.cs.ru.nl/~freek/comparison/comparison.pdf The Seventeen Provers of the World]" |
| 464310850 | 2011-12-06T01:04:20Z | Ruud Koot | /* References */ Freek Wiedijk. "[www.cs.ru.nl/~freek/comparison/comparison.pdf The Seventeen Provers of the World]" |
| 464040660 | 2011-12-04T13:45:06Z | 75.181.121.116 | /* Other proof assistants */ - alphabetizing list |
| 462902913 | 2011-11-28T14:46:56Z | Magmalex | /* Other proof assistants */ |
| 453733921 | 2011-10-03T17:42:32Z | Ruud Koot | /* See also */ [[Satisfiability Modulo Theories]] |
| 453538265 | 2011-10-02T15:06:41Z | 86.27.181.153 | |
| 451854797 | 2011-09-22T14:36:47Z | Ruud Koot | thumb size |
| 451854731 | 2011-09-22T14:36:25Z | Ruud Koot | /* Comparison */ [[Program extraction]] |
| 451847147 | 2011-09-22T13:42:51Z | Ruud Koot | [[Proof General]] |
| 451673367 | 2011-09-21T13:33:19Z | Ruud Koot | /* Other proof assistants */ lk |
| 451672276 | 2011-09-21T13:24:14Z | Ruud Koot | [http://matita.cs.unibo.it/ Matita] |
| 451634696 | 2011-09-21T07:17:53Z | Cydebot | Robot - Moving category Interactive theorem proving software to [[:Category:Proof assistants]] per [[WP:CFD|CFD]] at [[Wikipedia:Categories for discussion/Log/2011 September 14]]. |
| 450625379 | 2011-09-15T11:26:02Z | Ruud Koot | /* External links */ [http://www.cs.cmu.edu/~fp/lfs-impl.html Specific Logical Frameworks and Implementations] |
| 450624670 | 2011-09-15T11:18:21Z | Ruud Koot | fill table |
| 450526371 | 2011-09-14T20:21:34Z | Ruud Koot | /* Comparison */ NuPRL, LEGO |
| 450524124 | 2011-09-14T20:08:45Z | Ruud Koot | /* External links */ [http://www.nuprl.org/Intro/others.html NuPRL: Other Systems] |
| 450506907 | 2011-09-14T18:18:08Z | Ruud Koot | /* Comparison */ shorten links |
| 450506553 | 2011-09-14T18:15:49Z | Ruud Koot | /* Comparison */ fill table further |
| 450493949 | 2011-09-14T16:47:48Z | Pyschobbens | /* Comparison */ |
| 450493868 | 2011-09-14T16:47:16Z | Pyschobbens | /* Comparison */ |
| 450493683 | 2011-09-14T16:46:01Z | Pyschobbens | /* Comparison */ |
| 450493137 | 2011-09-14T16:42:04Z | Pyschobbens | /* Comparison */ |
| 450492833 | 2011-09-14T16:39:41Z | Pyschobbens | /* Comparison */ |
| 450401663 | 2011-09-14T02:24:32Z | Ruud Koot | /* Other proof assistants */ yarrow, typelab |
| 450401502 | 2011-09-14T02:22:55Z | Ruud Koot | /* References */ fix name |
| 450401442 | 2011-09-14T02:22:21Z | Ruud Koot | /* References */ [[Frank Pfennig]]. "The Practice of Logical Frameworks" |
| 450401241 | 2011-09-14T02:20:49Z | Ruud Koot | /* See also */ H. Geuvers. "Proof assistants: History, ideas and future". |
| 450400850 | 2011-09-14T02:17:31Z | Ruud Koot | /* External links */ dmoz |
| 450398566 | 2011-09-14T01:57:35Z | Ruud Koot | /* External links */ [http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html Interactive Theorem Proving for Agda Users] |
| 450395962 | 2011-09-14T01:35:54Z | Ruud Koot | /* External links */ lists of proof assistants |
| 450391239 | 2011-09-14T00:55:12Z | Ruud Koot | image of coq session |
| 450389545 | 2011-09-14T00:41:50Z | Ruud Koot | /* Comparison */ {{see also|Dependent type#Comparison|Automated theorem proving#Comparison}} |
| 450387447 | 2011-09-14T00:24:23Z | Ruud Koot | /* See also */ [[QED manifesto]] |
| 450385354 | 2011-09-14T00:07:26Z | Ruud Koot | copyedit |
| 450384846 | 2011-09-14T00:02:22Z | Ruud Koot | moved [[Interactive theorem proving]] to [[Proof assistant]] over redirect: more common name |
| 450384543 | 2011-09-13T23:59:44Z | Ruud Koot | /* Comparison */ {{see also|Dependent type#Comparison}} |
| 450382269 | 2011-09-13T23:39:59Z | Ruud Koot | /* Comparison */ |
| 450382214 | 2011-09-13T23:39:20Z | Ruud Koot | /* Comparison */ |
| 450381452 | 2011-09-13T23:31:46Z | Ruud Koot | properties of notable proof assistants |
| 450375795 | 2011-09-13T22:48:29Z | Ruud Koot | /* External links */ [http://adam.chlipala.net/cpdt/html/Intro.html "Introduction"] in ''Certified Programming with Dependent Types''. |
| 450365750 | 2011-09-13T21:43:30Z | Ruud Koot | /* See also */ [http://video.ias.edu/univalent/appel Introduction to the Coq Proof Assistant] (with a general introduction to interactive theorem proving) |
| 413367713 | 2011-02-11T21:28:50Z | Crisperdue | Link to TPS and ETPS |
| 379610568 | 2010-08-18T16:48:03Z | 95.146.60.8 | |
| 379610499 | 2010-08-18T16:47:34Z | 95.146.60.8 | |
| 366052817 | 2010-06-04T17:42:45Z | FrescoBot | Bot: links syntax and spacing |
| 359984650 | 2010-05-04T03:00:04Z | 77.11.14.222 | |
| 359984483 | 2010-05-04T02:58:55Z | 77.11.14.222 | |
| 347476514 | 2010-03-03T08:57:49Z | FrescoBot | Bot: links syntax |
| 331520121 | 2009-12-13T23:56:20Z | Galaxy07 | interwiki [[de:Maschinengestütztes Beweisen]] |
| 325903830 | 2009-11-15T02:07:45Z | 81.84.249.124 | |
| 325903802 | 2009-11-15T02:07:31Z | 81.84.249.124 | |
| 325903614 | 2009-11-15T02:06:05Z | 81.84.249.124 | |
| 325903469 | 2009-11-15T02:05:05Z | 81.84.249.124 | |
| 325903341 | 2009-11-15T02:04:04Z | 81.84.249.124 | Add mizar to the list of interactive theorem provers. |
| 279486202 | 2009-03-25T00:50:31Z | 89.176.209.188 | add Jape |
| 271801982 | 2009-02-19T11:11:17Z | 88.164.211.245 | /* See also */ redirection |
| 258542901 | 2008-12-17T09:36:42Z | 130.136.5.29 | Added a link to the Matita system |
| 226955178 | 2008-07-21T08:09:34Z | Classicalecon | |
| 200359154 | 2008-03-23T19:44:05Z | Arapajoe | |
| 177529059 | 2007-12-12T22:38:12Z | Greenrd | catsort |
| 177528998 | 2007-12-12T22:37:57Z | Greenrd | Added category |
| 163769026 | 2007-10-11T09:13:51Z | Tea2min | See also [[automated theorem proving]] |
| 162336894 | 2007-10-04T22:08:22Z | Dwheeler | Add PVS |
| 153713789 | 2007-08-26T09:47:58Z | CharlesGillingham | Fixing category hierarchies around Artificial intelligence |
| 153713735 | 2007-08-26T09:47:20Z | CharlesGillingham | fixing category hierarchies around Artificial intelligence |
| 146989198 | 2007-07-25T13:34:20Z | Hairy Dude | don't use horizontal rules |
| 146989084 | 2007-07-25T13:33:38Z | Hairy Dude | rm ellipsis (not encyclopaedic style) |
| 146988899 | 2007-07-25T13:32:27Z | Hairy Dude | don't put links in the title in the lede |
| 136831096 | 2007-06-08T14:01:43Z | Eubulide | MINLOG |
| 125805884 | 2007-04-25T11:50:22Z | 152.81.12.56 | |
| 105865089 | 2007-02-05T19:53:24Z | JenniferForUnity | Added some examples already in wikipedia. |
| 93582652 | 2006-12-11T14:42:15Z | MarSch | {{math-stub}} |
| 77641279 | 2006-09-25T01:39:34Z | Nicko6 | Better Stub |
| 77637775 | 2006-09-25T01:15:50Z | Toby Bartels | '''Proof assistant''' |
| 77603981 | 2006-09-24T21:34:12Z | Toby Bartels | {{stub}} |
| 62708958 | 2006-07-08T11:07:27Z | Scope creep | |
| 55916877 | 2006-05-30T12:23:20Z | Kku | |
| 17002213 | 2004-12-09T08:41:37Z | Charles Matthews | initial page |
