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: Sep 30 2023 at 06:01 UTC