Hacker News new | past | comments | ask | show | jobs | submit login

This turns out to be quite hard, because there are irreconcilable differences in the fundamentals of the different proof systems. That said, there's the Dedukti project, which is showing promising interop results between (at least) Coq and HOL style logics, and the work Mario Carneiro is doing trying to bridge between Metamath and more type-theory approaches.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact