Hacker News Reader

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.

View on HN

There 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

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.

Reply on news.ycombinator.com