Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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?

share|improve this question
    
Check Mizar. It was mentioned here several times. It is proof checker, input for it are formalized theorems and proofs, but language is near natural. So You may consider program which transforms proofs described in machine way You have mentioned above, into Mizar meta language, which is human readable and represents known mathematical facts, and it may be checked by Mizar system. –  kakaz Mar 16 '10 at 21:14
    
Mizar is a "smart" program as far as I see. It weights 27 megabytes and what I am asking for is a small stand-alone checker. I would tolerate primitive syntax as long as a formulation of a typical theorem is comprehendable. –  Sergei Ivanov Mar 16 '10 at 21:30
1  
What makes you think humans proof checkers are less buggy than computer ones? :) At least in a computer program, you only have to get it right once: a brain can make any number of different mistakes each time it runs. –  Max Jan 8 '11 at 22:39
4  
@Max: First, I have not seen a single bug-free program yet. Second, there are many human checkers but essentially only one machine checker for each proof. –  Sergei Ivanov Jan 9 '11 at 23:32
    
Certain kind of errors have to be accepted as part of human creativity- that is- overall - we all are humans and we are make mistakes but this is part of our living. It is worth of note that in certain situations errors and mistakes are not so important as statements which we say even with this errors in mind! Compare notes about David Hilbert works in famous G-C.Rota paper ams.org/notices/199701/comm-rota.pdf –  kakaz Feb 14 '11 at 12:23

9 Answers 9

up vote 21 down vote accepted

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.

share|improve this answer
1  
Do they address the "social" aspect of the question - that a human (not embedded deeply into the system) can check what is actually proved? That is, what is the formulation, definitions, and the axioms used - in a form readable by a human and verified by the simple core? How large are such data sets, actually? –  Sergei Ivanov Mar 16 '10 at 23:38
3  
You can understand what is proved, because the definitions and theorems have to be understandable for someone to write and prove them in the first place. The theorems are the same you'd find in a book, only written with quantifiers more explicit. The formal proof objects are (unfortunately) not understandable, because they contain too much low-level detail. Development sizes vary a lot. Surprisingly, fancy stuff (eg, constructive topology) is often shorter than basic mathematics (eg, arithmetic or group theory), since "basic" things rely on a much wider set of obvious mathematical facts. –  Neel Krishnaswami Mar 17 '10 at 11:47
    
Are formulations and axioms sent to the core checker in exactly the same form as they typed into the higher level system? I was under impression that the higher level system has some fancy input language that simplifies writing. (Maybe I confused it with Mizar.) –  Sergei Ivanov Mar 17 '10 at 17:38

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:

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 :(

share|improve this answer
    
You may ask for a Mizar source code, and You obtain it. There is one point: You have to write at least one Mizar "article" that is formalized proof before. Mizar is closed because it creator Andrzej Trybulec do not want any branching in the system. It is probably mistake but this is the state of affair. –  kakaz Feb 14 '11 at 7:29

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!

share|improve this answer

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.)

share|improve this answer
    
I don't see why pretty-printing is a problem. A standalone checker should just read its input files (human-readable definitions and statements and machine-generated proofs) and print "Yes" or "No" to the standard output. –  Sergei Ivanov Jan 9 '11 at 1:12
    
@Sergei: What the "ugly" proof that the checker reads is correct, but then when a human mathematician goes to look at the "pretty" printed result, a false statement has been printed? –  Daniel Litt Jan 9 '11 at 10:12
    
@Sergei: Yes, that is part of the job of the standalone checker, to print "yes" or "no". But there is a problem here: what exactly is it saying "yes" or "no" to? The exporter or importer may have made an error, and the unprinted theorem could establishing something else. In any case, the statement of the theorem and any definitions/axioms used need to be audited at some point, but the exporting system's printer cannot be trusted. It's far better for the checker to fully support the auditing process, regardless of the trustworthiness of the exporting system, the exporter or the importer. –  Mark Adams Jan 9 '11 at 14:09
    
@Daniel: It should not print the statement. It should verify the statement (which is written by a human). –  Sergei Ivanov Jan 9 '11 at 14:17
    
@Mark: If the definitions etc are to be audited by a human, they can as well be written down by a human. –  Sergei Ivanov Jan 9 '11 at 14:32

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.

share|improve this answer
1  
You have to add to those 300 lines the code of the python interpreter, and the code of the C compiler used to compile it, and the linker used to link it, and the libraries upon which it depends that are used at runtime, and the operating system the code runs on, and the microcode of the processors used, and the correctness of the actual chip! –  Mariano Suárez-Alvarez Mar 16 '10 at 22:43
13  
You forgot to mention the physical laws of the universe where the chip works. I don't think this is too big a problem as long as there are independent implementations of running on different hardware. Yes, and an alternative implementation of the universe, preferably open source. –  Sergei Ivanov Mar 16 '10 at 23:16
4  
Mariano and Sergei are just indicating two places to sit on the same issue. Sergei's question is "I am paranoid. Is everything definitely OK?" and Mariano's comment above is "You think you've got problems! I am very very paranoid and have realised I can never prove everything is OK". Mathematicians have to choose where to sit. –  Kevin Buzzard Mar 17 '10 at 7:17
12  
A related issue. Richard Pinch once told me that if you have a number p that you want to check is prime, and you start running a primality testing algorithm on it, then once the number is proved 99.999999999999% likely to be prime (e.g. because you've done 50 tests each one of which has a probability of 1/2 of failing if the number is composite) then before you do any more you might want to compare the probabilities you're dealing with, with the probability that little green men came down from Mars yesterday and replaced your computer with one where your code was replaced by buggy code. –  Kevin Buzzard Mar 17 '10 at 7:21
2  
mmverify's author is Raph Levien. –  Charles Stewart Mar 30 '10 at 9:31

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."

share|improve this answer

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.

share|improve this answer
    
Are these cores separate programs that make sense outside the whole system? Are proof objects text streams or objects of a high-level language in which the system is implemented in? –  Sergei Ivanov Mar 30 '10 at 11:03
    
@Sergei: Q1: often. Q2: when it comes to verification, the proof objects we are concerned with are usually text files that the user prepares, with or without the help of a proof editing assistant. These typically are, like Hilbert-style proofs, a list of assertions that build up to the conclusion, but typically there are gaps that the prover checks by performing some nontrivial (but usually decidable) computation to check. –  Charles Stewart Mar 30 '10 at 12:26
    
I meant the proof objects that are sent to the core. The core should not do anything nontrivial. –  Sergei Ivanov Mar 30 '10 at 13:05
    
@Sergei: The core should be a simple, easy to understand algorithm, but that does not mean it needs to be computationally trivial or inexpensive. I am not sure, but I think that proof checking for both LF and Gallina (Coq's core logic) are EXPTIME problems. –  Charles Stewart Mar 30 '10 at 15:53
    
Sergei, I asked Benjamin Gregoire (who is one of the main developers of Coq) and he said the 'kernel' is not as isolated as it could be, mainly for efficiency reasons. He also pointed out that someone recently implemented a standalone checker for Coq object files (.vo). See gforge.inria.fr/scm/viewvc.php/trunk/checker/?root=coq From logs the author seems to be lix.polytechnique.fr/~barras –  rgrig Apr 1 '10 at 12:18

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.

share|improve this answer
    
This self-verification idea is called "reflection". Harrison has proved the consistency of the HOL Light logical core (or, strictly speaking, a subset of the logical core) using HOL Light. As you say, this may use an incorrectness to justify itself, but it definitely gives confidence. This consistency proof has been successfully ported to my HOL Zero system, removing these concerns (although I have not audited the ported proof). A belt-and-braces approach is best of all worlds, combining reflective proofs, LCF-style inference kernels and porting proofs to trusted proof checkers. –  Mark Adams Jan 9 '11 at 14:40

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.)

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.