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: Feb 06 2023 at 12:04 UTC