Timeline for Proof of Giroux's correspondence
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 2, 2018 at 16:56 | comment | added | Paul | Thank you for your answers. I know that the vast majority of theorems haven’t been checked thoroughly down to the axioms. Rather the definition of theorem is “what the community agrees to be true” and the community tends to be tough. But still most theorems meet some standards (for example peer review process) which of course is not a total guarantee that they are true in a formal logic sense (recall Voevodsky famous non-theorem). But I agree that comments in MO are not the place for this discussion. | |
| Sep 2, 2018 at 9:22 | comment | added | Patrick Massot | Here is an exercise illustrating the importance of carefully reading what Giroux wrote. On page 409 you read "On épaissit ensuite le 1-squelette L de ∆ en une surface compacte F (presque) tangente à ξ le long de L". (I just copied this sentence into DeepL translator, and the translation is perfect!). Try to find this "presque" in other accounts of the story. Then prove, using only the definition of a contact form, that it shouldn't have been removed. | |
| Sep 2, 2018 at 9:17 | comment | added | Patrick Massot | About gaps in this particular proof, it's hard to tell, because the available sketch is so sketchy that it can't really be wrong. I never managed to surprise Giroux when discussing subtle points of the proof with him. There are real mistakes in attempted detailed exposition that have been mentioned here, but it's a bit unfair to insist on this point. So we have direct evidence that it's not easy for "any expert" to work out the details. | |
| Sep 2, 2018 at 9:11 | comment | added | Patrick Massot | It is considered a theorem because mathematical research is a complex sociological process involving large amounts of intuition and trust. Again this is a huge topic we cannot properly discuss here. And the publication status is not so relevant here. There are also published papers that are not trusted, although sometimes nobody has a specific error to point out. You can google "Coq mathcomp", "lean mathlib", "isabelle archive of formal proof" to get a sense of what is really verified in maths. But even there you'll need to convince yourself that definitions are correctly formalized. | |
| Sep 2, 2018 at 1:22 | history | edited | Chris Gerig | CC BY-SA 4.0 |
added 201 characters in body
|
| Sep 1, 2018 at 22:32 | comment | added | Paul | Or more directly, did you find significant gaps while writing the proof yourself? Or nothing that “any expert” could not work out? | |
| Sep 1, 2018 at 22:27 | vote | accept | Paul | ||
| Sep 1, 2018 at 19:48 | comment | added | Paul | Is there a chance that, for example, there is a gap that nobody has dealt with before? | |
| Sep 1, 2018 at 19:32 | comment | added | Paul | Thank you for your answer. I have not yet look through Goodman’s thesis but, if what you say is true (which I would not be surprised if it were) my question is, why is it considered a Theorem? And who would get the credit after a complete written proof was carried out? | |
| Sep 1, 2018 at 19:24 | history | answered | Patrick Massot | CC BY-SA 4.0 |