41

I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code. There are many levels of formal verification (that's the phrase you're looking for in place of "proven") of a proof assistant: Verify that the algorithms used by the proof assistant are correct. Verify ...


9

What you need is the idea of "the trusted core". Quoting "A verified runtime for a verified theorem prover": In many theorem provers, the trusted core—the code that must be right to ensure faithfulness—is quite small. As examples, HOL Light is an LCF-style system whose trusted core is 400 lines of Objective Caml, and Milawa is a Boyer-Moore style prover ...


6

While this may trend close to self-advertisement, this is essentially the topic of my recent paper Metamath Zero: The Cartesian Theorem Prover (video), and the analogy with bootstrapping compilers is spot on. The introduction of the paper lays out what is needed to make this happen, and it's only a problem of engineering. As Andrej says, there are several ...


3

In case you are not aware, there is a possibility that a theorem prover is implemented 100% correctly and run on a faultless machine and proves itself arithmetically inconsistent, even though it is not. The other existing answers focus on the issue of verifying that the theorem prover runs exactly as it was designed to run, but do not address this aspect of "...


1

If I recall correctly, this was chapter 5 or 6 of John Harrison's Handbook of Practical Logic and Automated Reasoning. Jon Sterling wrote some notes for a recitation a year or two back, specifically for an LCF prover using sequent calculus.


1

Here are some thoughts and code from the kernel (file thm.ML in Isabelle/Pure) from Isabelle: abstype thm = Thm of deriv * (*derivation*) {cert: Context.certificate, (*background theory certificate*) tags: Properties.T, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or ...


Only top voted, non community-wiki answers of a minimum length are eligible