This question is actually easy.
HOL Light, in the tradition of so-called "LCF-style" proof assistants, checks proofs by using an abstract datatype for theorems whose only constructors are inference rules.
You can see this in the file "fusion.ml
", which, being the only ML code one needs to trust (presuming you trust your ML environment) to believe that HOL Light thms are theorems of higher order logic, is relatively well-written and easy to read.
In particular, notice that in the module signature the type thm is abstract (it doesn't say "type thm = something", just "type thm") and the only functions that return thms (at the bottom) are inference rules (REFL, TRANS, etc.), definitional rules (new_basic_definition, etc.) and axioms (new_axiom).
Since OCaml modules are "closed", when the module type signature ends and there's nothing else to generate thms, we know those are the only ways thms will ever be generated.
Thus, no matter how clever the code you use to generate your proofs (be it miz3, normal HOL Light tactics, or something else), ultimately, if that code generates any thms, what it has to do is steer the so-called "kernel" in fusion.ml
by calling the inference/definition rules and new_axiom, possibly using existing theorems and existing derived rules (which do the same thing), in clever ways to construct the desired thms. The kernel is designed so that doing so is equivalent to running line-by-line down a proof in higher order logic.
In the implementation of the rules you can check that they do what they ought to.
In particular, new_axiom records any axioms in the list !the_axioms, so you can check axioms() to be sure you nobody added unsound axioms to prove your theorems. the_axioms itself is in the module and not the signature, so the only access to it outside of fusion.ml
is read-only via axioms (which is in the signature), thus the list can only grow, and axioms used along the way can't be removed and hidden.
As you may have inferred, while thms are OCaml objects that you can store and play with, and we have a story for why they can only be created in ways guaranteeing that they have proofs, the proofs themselves are dynamic and ephemeral. If you want to see/keep the (ultra low level) proofs as well, you could use Joe Hurd's fork of HOL Light (http://src.gilith.com/hol-light.html
) which records the proofs and enables export in OpenTheory Article format (http://www.gilith.com/research/opentheory/article.html
This is why sometimes people let LCF-style proofs become "unreadable": no matter whether you write readable (maybe even declarative) programs for constructing thms or whether you write totally unreadable (but possibly efficient, or smart, or good for exploration and automation) code for constructing thms, there will always be this (ephemeral) ultra low level proof that is the "real" proof of your theorem in the formal sense. There are arguments on both sides for prioritising readability of the programs or not.