Lean can export fully elaborated proof terms https://github.com/leanprover/lean/blob/master/doc/export_format.md and there are external type checkers for those terms. Is there something similar for Coq?

Kind of. There is no separate file format, since `.vo`

already contains the elaborated proof terms. And the program is called `coqchk`

. It is a smaller version of Coq's kernel.

Last updated: Jun 25 2024 at 18:02 UTC