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 FeitThompson (oddorder) 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 