Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-11-07

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #isabelle
02:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
03:50 tokenrove joined #isabelle
05:56 dmiles_afk joined #isabelle
13:48 dmiles_afk can the four color theorem setup of Coq be tranlated to Isabelle?
14:12 ThreeOfEight dmiles_afk: I doubt it
14:12 ThreeOfEight the Coq formalisation would probably be helpful, but Isabelle's logic differs hugely from HOL
14:12 ThreeOfEight er, from Coq
14:13 ThreeOfEight by which I mean Isabelle/HOL's logic differs hugely from Coq, but since Isabelle doesn't really support dependent types, no logic of Isabelle could be similar to Coq, I should think
14:14 ThreeOfEight but as I said, the formal definitions and statements of auxiliary lemmas in Coq alone would probably be helpful when creating a formalisation in Isabelle
14:14 ThreeOfEight I've ported some HOL Light proofs that I didn't understand at all, but just looking at the statements of the intermediate auxiliary lemmas was very helpful
14:25 dmiles_afk myt real agenda is to find our how i can represent the conjecture in first order logic
14:26 dmiles_afk though maybe Coq is closer to FOL
14:27 dmiles_afk part of the difficualy though is understanding how to set it up .. does one bit of FOL do map generations, and another bit "test" them ?
14:28 dmiles_afk sorry, my question is way out of scope for hte channel.. but i did mean to cauasuly find out if the systems mmeet at the proof general level easiliy
14:29 dmiles_afk so you've said that Isabelle and Coq  meet at HOL Light.. but that doesnt make them interchangable
14:30 dmiles_afk also i dont even know if HOL Light and FOL are vaugly compatible
14:31 dmiles_afk hehe so any scrapts of common sense about any of these things is helpfull
14:50 ThreeOfEight dmiles_afk: huh?
14:50 ThreeOfEight they "meet at HOL Light"?
14:50 ThreeOfEight I don't know what that means. When did I say that?
14:51 ThreeOfEight and I don't know much about FOL and the Four Colour Theorem
14:51 dmiles_afk you said they "dont meet at HOL light"
14:51 dmiles_afk I've ported some HOL Light proofs that I didn't understand at all, but just looking at the statements of the intermediate auxiliary lemmas was very helpful
14:52 dmiles_afk well acvutlay you said they met.. but not really a comfortable meeting
14:54 dmiles_afk So they would round trip?
14:54 dmiles_afk round trip convert between the two systems without dataloss
14:55 dmiles_afk round trip = convert between the two systems without dataloss .. or maybe there is dataloss converting from Coq->Isabelle->Coq
14:56 dmiles_afk but if Coq passes along the aux lemmes it used and Isabelle was OK with that.. then there would be no loss
14:59 dmiles_afk I'll try to phrase my further questions in the form of questions
15:00 dmiles_afk Since Isabelle doesn't really support dependent types, does the aux lemmes passed along help supliment Isabelle?
15:04 ThreeOfEight well you probably can't write the definitions and the lemmas in the same way in Isabelle as you do in Coq
15:05 ThreeOfEight but just seeing what kind of auxiliary lemmas are needed and how certain concepts are formalised help you a lot
15:05 ThreeOfEight when you formalise a mathematical theorem, a huge part of the problem is "what proof approach do I choose", "how do I write down this reasoning formally", "how do I define things best to get smooth proofs" etc.
15:06 ThreeOfEight often you have several different ways to phrase some fact or to define some constant, but some of them are easier to work with in a formal setting than others
15:06 ThreeOfEight if somebody else has already done that work in another prover (and chased down all the dead ends), that makes things easier
15:07 dmiles_afk "Hales and Gonthier have use modern theorem provers (Isabelle, Coq, and HOL) to formally prove the Four color theorem, the Feit-Thompson (odd-order) theorem, and the Kepler conjecture."   wonder if there was 3 systems each proving one of those
15:08 dmiles_afk or if that says the 4CT was once done in all three
15:22 ThreeOfEight not really
15:23 ThreeOfEight Feit Thompson and Four Colour theorem was both Coq
15:23 ThreeOfEight Kepler conjecture was mostly HOL Light and some parts done in Isabelle
15:24 ThreeOfEight as for the Kepler conjecture, there's the official report here: http://arxiv.org/abs/1501.02155
15:32 dmiles_afk nice, that paper will help me

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary