Timeline for Endless controversy about the correctness of significant papers
Current License: CC BY-SA 3.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 27, 2017 at 20:03 | comment | added | Steve Huntsman | It's perhaps worth noting that there is a document called "Defects in the revised definition of Standard ML" that, while it doesn't refer to OCaml, certainly ought to highlight that even a language that is "precisely defined" enough to have a book devoted to the definition has some lacunae. | |
| Oct 16, 2017 at 9:29 | comment | added | James Smith | Hi, Timothy. I was referring to the software that made the numerical calculations this time, as you rightly point out. But yes, since all of the software was verified with a verifier written in OCAML, of course there is still an element of doubt. There's no need to apologise for being pedantic, it's par for the course. | |
| Oct 16, 2017 at 1:35 | comment | added | Timothy Chow | @JamesSmith : Sorry to be pedantic, but I think people could get confused by your statement that "the software making the calculations was also verified." This is true in the sense that the calculations aren't just being executed by some C code or something, but are being subject to verification by the proof assistant. But on the other hand, everything is being programmed and run in OCAML, and it is not the case that the implementation of OCAML has been formally verified to be correct. | |
| Oct 15, 2017 at 20:21 | comment | added | James Smith | Sorry one more thing I should mention to no-one in particular. On re-reading your answer, I see shades of my belief that the acceptance or otherwise of a complex and lengthy proof is not necessarily settled by formal verification. I've written elsewhere that I think that this is as much of a cultural issue as a technical one but again I can't find the words. However, I do strongly believe that it is bound, at least in part, to the accessibility of the software to mathematicians who aren't experts in formal verification. | |
| Oct 15, 2017 at 20:15 | comment | added | James Smith | Leaving that aside, I couldn't prove the Kepler conjecture to my own satisfaction because the amount of effort to assemble and run the software to verify it is considerable. I simply gave up. In my humble opinion the blueprint proof will really come to life when the software used to verify it is simple and accessible to non-experts. We are still some way from that. A distance ambition of mine is to see it happen, though. | |
| Oct 15, 2017 at 20:11 | comment | added | James Smith | I agree. However, it is worth pointing out in passing that the software making the calculations was also verified as part of the Flyspeck project. | |
| Oct 15, 2017 at 19:18 | comment | added | Timothy Chow | @JamesSmith : Some time ago Harrison provided a verification of the HOL Light kernel without definitions. However, since HOL Light runs (or originally ran) on top of OCAML, you might wonder about the correctness of OCAML. On the bright side, I gather that there has been some progress in this direction since 2008, e.g., link.springer.com/chapter/10.1007/978-3-319-08970-6_20 Regarding the "blueprint proof," it is humanly comprehensible, but there is still an enormous computer calculation involved whose results you simply have to trust. | |
| Oct 15, 2017 at 12:46 | comment | added | James Smith | I think the whole point of Hale's blueprint proof is that it is humanly comprehensible, certainly so compared to the original submitted to Annals. I've posted a link to Hale's own talk on the subject somewhere on this page, so I think best not to post it again, but it is well worth watching. It is interesting to note your comments about HOL light not itself being fully trustworthy. I didn't know that, I had assumed that it was. | |
| Oct 6, 2017 at 2:54 | comment | added | Lucia | @SteveHuntsman: All correct proofs are alike; every incorrect proof is incorrect in its own way? | |
| Oct 5, 2017 at 21:14 | comment | added | Steve Huntsman | This reminds me of de Branges | |
| S Oct 5, 2017 at 16:12 | history | answered | Timothy Chow | CC BY-SA 3.0 | |
| S Oct 5, 2017 at 16:12 | history | made wiki | Post Made Community Wiki by Timothy Chow |