4 ms·
I don't work in this field, but I would like to know out of lay interest. Are there translators that to convert proofs in one system to another? Such a translat
by lake99 8y ago
I don't work in this field, but I would like to know out of lay interest. Are there translators that to convert proofs in one system to another? Such a translator would prove (pardon!) to be useful to collaborating researchers.
I know that these systems each have unique features, so I don't mean a 100% translation. For the purposes of this question, translating proofs for the intersection of features would suffice.
- dwheeler 8y agoThere has been some work to translate between systems. For example, see "Conversion of HOL Light proofs into Metamath" by Mario Carneiro, 2014: https://arxiv.org/abs/1412.8091 https://arxiv.org/abs/1412.8091 However, it turns out to be non-trivial, so it is not typically done in practice. Formalization requires very precise specification, and even slight differences can cause complications. But like many other things, who knows, perhaps there will be further progress in this area.