5 ms·

We have a bunch of theorem provers - Lean, Coq, Agda, Isabelle If you prove something in Lean, can you automatically convert the proof into a Coq one (even if

We have a bunch of theorem provers - Lean, Coq, Agda, Isabelle If you prove something in Lean, can you automatically convert the proof into a Coq one (even if it looks like uglyfied/minified code)? It feels like it should be possible to "merge" the proof repositories of these languages together into a common one. Or to put another way, if you can prove in Coq that Lean is correct, then it should imply that Lean proofs are correct too.

drdeca 7y ago
I asked a similar question in the comments on a youtube video, and Mario Carneiro, one of the people who work on Lean, answered me. He said he does work on this area, and it kind of works (at least for the theorems you would want to translate?), but in addition to the proofs being very not nice to read, the way the statements of the theorems are translated are, by default, also rather not nice (being statements about specific formulations of the objects (such as the set of integers) as they are expressed/defined in the language being translated from, instead of referring to the corresponding objects that have been defined in the language being translated to. However, he says that it doesn’t take all that much work to manually massage it until the statement of the theorem is expressed in the way that you want it to be. I’m on my phone right now, and the phone youtube app doesn’t give me a permalink, but I’ll try and edit this comment soon on laptop to include link to the comment section. Edit : here are links to what Mario Carneiro said in the thread click the read all replies to read the full thread) https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S8caeH54AaABAg.9-lfXqsNEk29-wEI6kwEni https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S... https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S8caeH54AaABAg.9-lfXqsNEk29-wJfoexc7_ https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S...

drdeca 7y ago

I asked a similar question in the comments on a youtube video, and Mario Carneiro, one of the people who work on Lean, answered me. He said he does work on this area, and it kind of works (at least for the theorems you would want to translate?), but in addition to the proofs being very not nice to read, the way the statements of the theorems are translated are, by default, also rather not nice (being statements about specific formulations of the objects (such as the set of integers) as they are expressed/defined in the language being translated from, instead of referring to the corresponding objects that have been defined in the language being translated to. However, he says that it doesn’t take all that much work to manually massage it until the statement of the theorem is expressed in the way that you want it to be. I’m on my phone right now, and the phone youtube app doesn’t give me a permalink, but I’ll try and edit this comment soon on laptop to include link to the comment section. Edit : here are links to what Mario Carneiro said in the thread click the read all replies to read the full thread) https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S8caeH54AaABAg.9-lfXqsNEk29-wEI6kwEni https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S... https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S8caeH54AaABAg.9-lfXqsNEk29-wJfoexc7_ https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S...