Timeline for How true are theorems proved by Coq?
Current License: CC BY-SA 4.0
22 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 23, 2023 at 14:41 | answer | added | joro | timeline score: 1 | |
| Nov 28, 2021 at 10:27 | comment | added | Guy Coder | For those interested in Proof Assistants, there is a new proposed SE site ProofAssistants | |
| Nov 2, 2021 at 9:39 | history | edited | Martin Sleziak | CC BY-SA 4.0 |
changed mobile Wikipedia link to the full site
|
| Oct 31, 2021 at 22:10 | comment | added | David Roberts♦ | @joro well Lean defines division by 0 as some specific value, so that $(-)/(-)$ is a total function, but the field axioms only apply to the usual, sensible values of division (one has to supply a reference to the fact/proof the denominator is nonzero, when this counts). This is purely a computer science implementation issue, much like how 3 is a topology on 2 in ZFC, using the von Neumann finite ordinals. | |
| Oct 31, 2021 at 14:23 | comment | added | joro | @DavidRoberts The border case modulo zero suggests at most one of {coq,isabelle} is correct: mathoverflow.net/questions/82181/… | |
| Oct 31, 2021 at 9:13 | comment | added | David Roberts♦ | Yes, I vaguely recall that there have been outright (local) bugs. | |
| Oct 31, 2021 at 8:51 | comment | added | joro | @DavidRoberts Thanks. Many years ago on the Coq mailing list I saw proof based on paradox of the form A = not A which raised error of the form "multiverse inconsistency" | |
| Oct 31, 2021 at 8:41 | comment | added | David Roberts♦ | @joro I recently watched a talk about MetaCoq, which is trying to verify Coq, and apparently there's a whole lot that's not even documented, let alone the full formal system being described anyway. | |
| Oct 31, 2021 at 1:32 | history | edited | David Roberts♦ | CC BY-SA 4.0 |
more permanent reference
|
| Jan 15, 2019 at 1:41 | answer | added | David Roberts♦ | timeline score: 6 | |
| S Aug 15, 2017 at 16:32 | history | suggested | Martin Sleziak |
added (proof-assistants) and (coq) tags
|
|
| Aug 15, 2017 at 16:15 | review | Suggested edits | |||
| S Aug 15, 2017 at 16:32 | |||||
| May 29, 2015 at 17:03 | answer | added | cody | timeline score: 18 | |
| May 29, 2015 at 8:31 | answer | added | David Roberts♦ | timeline score: 3 | |
| Jun 15, 2011 at 7:53 | comment | added | joro | David: I thought you would be more interested in the Pollack quote. According to Pollack what you consider "underlying formal system" has "informally specified " coercions that may be used in proofs. An interesting question is "where is the full formal system of Coq described/proved" (I couldn't find such, found articles covering parts of the code...) | |
| Jun 15, 2011 at 7:22 | vote | accept | David Roberts♦ | ||
| Jun 15, 2011 at 6:30 | answer | added | joro | timeline score: 11 | |
| Mar 25, 2011 at 16:02 | answer | added | Timothy Chow | timeline score: 46 | |
| Mar 25, 2011 at 15:01 | comment | added | darij grinberg | As far as I have been taught, Coq proofs are pretty much the best proofs you can get: they just require intuitionistic logic in the strong sense (not the Russian one). Of course, I don't know what the "popular packages" are and whether one of them smuggles in some ZFC... | |
| Mar 25, 2011 at 14:03 | answer | added | Stefan Geschke | timeline score: 8 | |
| Mar 25, 2011 at 7:05 | answer | added | Julien Puydt | timeline score: 6 | |
| Mar 25, 2011 at 5:57 | history | asked | David Roberts♦ | CC BY-SA 2.5 |