How do they verify a verifier of formalized proofs?

Question

In an unrelated thread Sam Nead intrigued me by mentioning a formalized proof of the Jordan curve theorem. I then found that there are at least two, made on two different systems. This is quite an achievement, but is it of any use for a mathematician like me? (No this is not what I am asking, the actual question is at the end.)

I'd like to trust the theorems I use. To this end, I can read a proof myself (the preferred way, but sometimes hard to do) or believe experts (a slippery road). If I knew little about topology but occasionally needed the Jordan theorem, a machine-verified proof could give me a better option (and even if I am willing to trust experts, I could ensure that there are no hidden assumptions obvious to experts but unknown to me).

But how to make sure that a machine verified the proof correctly? The verifying program is too complex to be trusted. A solution is of course that this smart program generates a long, unreadable proof that can be verified by a dumb program (so dumb that an amateur programmer could write or check it). I mean a program that performs only primitive syntax operations like "plug assertions 15 and 28 into scheme 9". This "dumb" part should be independent of the "smart" part.

Given such a system, I could check axioms, definitions and the statement of the theorem, feed the dumb program (whose operation I can comprehend) with these formulations and the long proof, and see if it succeeds. That would convince me that the proof is indeed verified.

However I found no traces of this "dumb" part of the system. And I understand that designing one may be hard. Because the language used by the system should be both human-friendly (so that a human can verify that the definitions are correct) and computer-friendly (so that a dumb program can parse it). And the definitions should be chosen carefully - I don't want to dig through a particular construction of the reals from rationals to make sure that this is indeed the reals that I know.

Sorry for this philosophy, here is the question at last. Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their systems trustable?

UPDATE: Thank you all for interesting answers. Let me clarify that the main focus is interoperability with a human mathematician (who is not necessarily an expert in logic). It seems that this is close to interoperability between systems - if formal languages accepted by core checkers are indeed simple, then it should be easy to automatically translate between them.

For example, suppose that one wants to stay within symbolic logic based on simple substitutions and axioms from some logic book. It seems easy to write down these logical axioms plus ZF axioms, basic properties (axioms) of the reals and the plane, some definitions from topology, and finally the statement of the Jordan curve theorem. If the syntax is reasonable, it should be easy to write a program verifying that another stream of bytes represents a deduction of the stated theorem from the listed axioms. Can systems like Mizar, Coq, etc, generate input for such a program? Can they produce proofs verifiable by cores of other systems?

Answer 1

Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their systems trustable?

This is called the "de Bruijn criterion" for a proof assistant -- just as you say, we want a simple proof checker, which should be independent of the other machinery. The theorem provers which most directly embody this methodology are those in the LCF tradition, such as Isabelle and HOL/Light. They actually work by generating proof objects via whatever program you care to write, and sending that to a small core to check. Systems based on dependent type theory (such as Coq) tend to have more complex logical cores (due to the much greater flexibility of the underlying logic), but even here a core typechecker can fit in a couple of thousand lines of code, which can easily be (and have been) understood and reimplemented.

Answer 2

You are asking a lot of great questions:

[Are computer proof assistants] any use for a mathematician like me?

Yes. Here is how these systems can help you:

• On a very basic level, these systems prevent you from making mistakes. Subsequently, it spares one from the peer review process. One of the proofs of Jordan Curve theorem was carried out by Thomas Hales, as part of his attempt to automatically verify the correctness of the Kepler Conjecture. Hales is basically resorting to automated theorem proving because he feels that his proof, which involves establishing that 50,000 linear programming problems are infeasible (last time I checked) cannot possibly be verified by human peer review.

• Most systems (Coq, Isabelle, HOL-Light) built in automation. This helps to inform the informal notion that mathematicians have for what constitutes a trivial, mechanical derivation and what is nontrivial - my rule of thumb is, if a computer can't automatically derive a certain, it's probably something I should illustrate explicitly.

• Isabelle/HOL lets you use the automated theorem provers E, SPASS and Vampire to automatically prove propositions, employing the entirety of Isabelle/HOL's Library at their disposal. As Isabelle's library grows, this gains more and more power.

But how to make sure that a machine verified the proof correctly?

As Neel Krishnaswami mentioned above, one way one may be convinced is to learn how to program in pure, functional programming languages such as OCAML or SML and read the source code of systems like HOL-light or Isabelle. In both of these systems I have mentioned, there is a file thm.ml that contains the declarations of theorem constructors. These systems also have facilities for declaring new types. HOL-Light has, along with the basic rules and type constructors, three axioms: extensionality (Liebniz's Law), the axiom of infinity and the axiom of choice.

Moreover, HOL-Light has been designed by it's author John Harrison to exhibit relative self-consistency proofs, just like in set theory. You may read about them here: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.2210&rep=rep1&type=pdf

Here Harrison shows HOL-Light$-$Infinity has a model in HOL-Light, and HOL-Light has a model in HOL-Light+Grothendiek Cardinal.

The definitions should be chosen carefully - I don't want to dig through a particular construction of the reals from rationals to make sure that this is indeed the reals that I know.

I assume you are aware that all complete ordered fields are isomorphic to one another? Isabelle/HOL happens to construct them using Cauchy sequences, and has in its library there is another formulation using Dedekind Cuts. HOL-Light formulates the positive reals using the limiting slopes of functions $f:\mathbb{N}\to\mathbb{N}$ and then constructs the full reals using a semi-ring completion. Since algebraically all of these formulations are provably isomorphic, in practice the details of their construction are hidden from the users.

Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their systems trustable?

They all require training to learn. However, for LCF style systems like Coq, Isabelle, and HOL-Light, its like programming languages: once you learn one, you've learned the principles necessary to understand all of them.

Isabelle, and Mizar have special facilities for making proofs more "human". The system for Isabelle is called Isar. These systems aren't for dummies, sadly; one really needs a bit of special training to master them. On the other hand, they are much better than the "apply-style" proofs that are commonly employed, since they conform much better to human intuition. There's a systems for Coq called Caesar that in its infancy, but I expect it will ultimately make Coq much easier to use.

If the syntax is reasonable, it should be easy to write a program verifying that another stream of bytes represents a deduction of the stated theorem from the listed axioms. Can systems like Mizar, Coq, etc, generate input for such a program? Can they produce proofs verifiable by cores of other systems?

The short answer is YES, the long answer is YES, but it's complicated. Not all deductive systems have the same expressive power. Sets in ZFC are a special kind of object that one cannot construct in Higher Order Logic. To formulate set theory in Isabelle/HOL and HOL-Light use, one needs to postulate that a kind of object that makes true the axioms of Zermelo Fraenkel set theory exists (this is the route that Isabelle/HOLZF takes). On the other hand, one may embed HOL into ZFC without such difficulty - here is a paper where a translation system for Isabelle/HOL into ZFC is given using the theorem prover LF: http://kwarc.info/frabe/Research/RI_isabelle_10.pdf

Chantal Keller has imported HOL-Light into Coq in her MSc thesis here: http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf

Importing back from Coq is difficult. Coq has a much more expressive type system than HOL.

HOL-Light and Isabelle/HOL can be inter-translated, however:

• Isabelle/HOL to HOL-Light: http://www.cs.cmu.edu/~seanmcl/papers/modules.pdf
• HOL-Light to Isabelle/HOL: http://www.springerlink.com/content/m7621r5258r8n711/

One cannot convert Mizar proofs to any other system because it is closed source, and does not have a small kernel one can use to produce proof code readable by other engines :(

Answer 3

This answer is really an augmentation of Neel's (but too long to fit in a comment). The "de Bruijn criterion" was so-named by his colleague Henk Barendregt in the paper Autarkic Computations in Formal Proof (with Erik Barendsen) from 1997. However this is really implicit in de Bruijn's work, see for example The Mathematical Language AUTOMATH, its Usage, and Some of its Extensions from 1968. The AUTOMATH archive should really be required reading for anyone interested in computer-assisted deduction (as so many people are still re-discovering what de Bruijn already knew 40 years ago).

Of course, the Barendregt/Barendsen article is interesting in its own right, as it advocates the use of computations as legitimate parts of proofs, something mathematicians do routinely, but proof systems based on the "de Bruijn criterion" and the LCF approach shy away from -- until recently. They dub this the Poincare Principle (which I certainly adhere to). Both Coq and Isabelle have started doing more and more computations. The purists in the theorem proving community used to look down on PVS and before that IMPS for doing ``too much'' computation!

Answer 4

I think the question you are asking - about how can we trust a formal proof - is a very important question. I have spent considerable effort developing software to specifically address this question. You touch on various things I have concentrated on.

It is true that various systems prominent in the formalisation of mathematics - including the HOL systems (HOL4, ProofPower HOL, HOL Light), Isabelle and Coq - are built according to the "LCF style", which means that all deduction must go via a relatively small kernel of trusted source code (implementing the primitive inference rules), and that this greatly reduces the risks of producing unsound proofs on these systems. It would also not be an exaggeration to say that almost everyone working in formal proof is happy with this situation. Indeed, probably most (but not those working on the above systems) feel that resorting to the LCF style is overkill and an unnecessary drain on user execution time and on development effort.

However, there are 3 major problems with this status quo:

A) Most "LCF-style" systems do not implement the LCF-style kernel idea as purely as may be expected. Some systems have back doors to creating "proved theorems", such as importing the statements (but not the proofs) of previously proved results from disk, and trust that the user will not abuse this. Also, to reduce execution time, most systems implement various derivable inference rules as primitives, multiplying up the size of the trusted source code. Also, the kernels of most systems typically incorporate large amounts of supporting code (e.g. for organising theories) and are not particularly clearly implemented, and so are difficult to review. It should be noted that HOL Light does not suffer from any of these problems.

B) The trusted aspects of an LCF-style system is NOT limited to the design/implementation of its LCF-style kernel. Like in all systems, it at least also includes the design of the concrete syntax and the implementation of the pretty printer, since, in practice, the user will only view results displayed in concrete syntax via the pretty printer. However, each system has problems with its concrete syntax and/or pretty printer that allows misleading information to be displayed to the user (e.g. by using irregular variables names, or names that are overloaded). I have found many ways of appearing to prove "false" in these systems! Also, depending on how the system is used, the parser is arguably also a trusted component.

C) The importance of the human process of checking that the intended result has in fact been proved (I call this "proof auditing") is generally greatly underestimated, and in practice often not even carried out at all. As you rightly point out, the axioms and definitions used in a formal proof need to be carefully checked, as well as the statement of the theorem itself. I have known subtle mistakes in definitions to render real formal proofs on real projects completely invalid.

I have developed an open source theorem prover called HOL Zero, that addresses issues A-C above and is designed for use in proof auditing and generally to be as trustworthy as possible. It has a watertight inference kernel, a well-designed concrete syntax and pretty printer, and the source code aims to be as clear and well-commented as possible. However, it should be noted that it does not have the advanced automatic and/or interactive proof facilities of the existing systems I mention above, and is not suited to developing large formal proofs. HOL Zero can be downloaded from here (it needs OCaml and a Unix-like operating system):

http://www.proof-technologies.com/holzero

The concept of checking one system using another is not only philosophically reassuring, but also of pressing need (due to the above issues A-C). As you say, what is needed is the ability to port proof objects between systems (the so called "de Bruijn criterion"). Strictly speaking, the de Bruijn criterion is as you state your requirement - the ability to capture a proof as an object (e.g. a text file) - rather than the LCF style (but let's not get too philosophical about the equivalence of these approaches). Anyway, there are some practical issues here:

1. The "dumb program" that you refer to needs to be surprisingly sophisticated, otherwise it loses much of its purpose. If it is just an LCF-style kernel, the data it outputs will be too slow to review for large projects. As you say, it needs to be human-friendly - a decent pretty printer is a practical necessity. Also, to make proof exporting (see next item) work in practice, it needs to work at least at a slightly higher level than the kernel, and so some supporting theory is required to be built. So yes, a dumb program is required, which should be as easy to understand as possible, but it is more challenging to build than a few lines of code.

2. Capturing proof objects in a suitably efficient way is a non-trivial exercise. The work that others mention above successfully port things like the base system of HOL Light, but are completely incapable of handling something the scale of Hale's HOL Light proof of the Jordan Curve Theorem, let alone Hale's Flyspeck Project (using HOL Light to check his non-formal proof of the Kepler Conjecture).

3. Some sort of neat and trivial correspondence of equivalent theory between systems is useful. This is better than importing language statements as huge expressions, in terms of some highly-complex embedding of one notation inside another, which would either greatly increase the complexity of the checking system or make its human usage difficult.

HOL Zero is primarily aimed at the "dumb program" proof checker role. The idea is it will import and replay proofs that have been exported from other HOL systems. I have implemented a proof exporting mechanism which, unlike others' mechanisms, handles with ease large proofs such as Hale's Jordan Curve proof and the (almost-complete) Flyspeck Project. I am currently working on a proof importing mechanism for HOL Zero. (Note that a former proof importing mechanism I developed worked on an old version of HOL Zero and successfully ported Hale's Jordan Curve proof and Harrison's proof of the consistency of the HOL Light kernel.)

Answer 5

Arguably Norman Megill's Metamath http://metamath.org/ is not a mainstream proof verifier. But various third parties have written short programs to check his deductions, starting with Ralph Lieven's mmverify program which is 300 lines of Python; surely short enough for an interested bystander to survey.

Answer 6

See question #5 in the Coq FAQ:

http://coq.inria.fr/faq

"You have to trust that the implementation of the Coq kernel mirrors the theory behind Coq. The kernel is intentionally small to limit the risk of conceptual or accidental implementation bugs."

Answer 7

The key point is the idea of the kernel of a theorem prover, as Adam mentioned. To put it another way the kernel is the smallest subset of the theorem prover's code base (and operating system and machine's physical realisation) that has the property that if the theorem prover proves a false theorem, then there is an error in the kernel that is responsible. Identifying the kernel is a matter of computer science, and errors in our grasp of computer science might lead us to misidentify the kernel.

Beyond the confidence one has in a particular implementation's realisation on a particular machine, note:

1. The important theorem provers are multiply realised: many operating systems running on many machine architectures run the theorem proving code. So errors in the kernel that are due to the operating system or physical machinery must be ones that arise multiply, either by coincidence or by shared errors of design.
2. Theorem provers with the small core Neel describes (which includes all the important ones) can themselves be proven correct, giving a correctness proof that can be checked by other theorem provers. Less is done here than should have been done — I have heard that the Coq in Coq certification has been checked in Twelf, but have no reference — but in principle this observation means that errors in the kernel arising in the implementation of the theorem prover itself must also arise multiply among the theorem provers that verify the correctness proof.

I recommend Geuvers (2009)'s Proof assistants: History, ideas, and future for an overview of these, among other other, issues.

Answer 8

One simple suggestion no-one seems to have mentioned is to have the verifier prove itself correct.

Obviously, this cannot really give any assurance that the verifier is correct, since if the verifier is incorrect its proofs are worthless. However, on heuristic grounds, this should give some confidence. The reason is that errors in assertions about the verifier's proofs (which will be checked) should be uncorrelated with the errors in the verifier itself.

Of course, no physical process can be expected to prove anything with complete accuracy, so these kind of heuristics are the best one can hope for anyway.

Answer 9

Many pointed out the essential: Provers like Coq and HOL have a very small core that checks the proofs.

I want to add that there are other provers, the 'automatic' ones, which do indeed tend to be complicated. For example, most SMT solvers are like that. The route taken there is exactly the one mentioned in the question. Instead of trying to verify the proof 'finder', they modify it to generate proofs that can be checked by a very small proof checker. (See this article.)