User mark adams - MathOverflow

Answer by Mark Adams for How do they verify a verifier of formalized proofs?

2011-01-08T22:05:09Z

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:

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.
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).
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 by Mark Adams for How do proof verifiers work?

2011-01-08T19:47:20Z

Hope I'm not too late to help, but....

As far as I know, the proof verifiers most extensively used in serious mathematics formalisation are the HOL systems (HOL4, ProofPower HOL, HOL Light), Isabelle, Coq and Mizar. Unlike the others, Isabelle can be configured with the logic it supports, but the only two logics with significant support are HOL and ZF. The HOL logic is classical, higher-order and polymorphically (but not dependently) typed. Isabelle ZF is classical, first-order and not typed. Coq's logic is intuitionistic, higher-order and polymorphically and dependently typed. Mizar's logic is classical, second-order and not typed (I think). All these systems except Mizar are implemented in the "LCF-style", which means that their logical soundness depends on only a relatively small kernel of source code.

Except for Mizar, these systems are all open source and implemented in functional programming languages (e.g. ML, Lisp, Haskell). Assuming you know a little about functional programming, the best way to get a good concrete understanding is to examine their source code, but this will take a huge amount of time because their implementations are large, complicated and poorly documented. However HOL Light (the principal system used in Hale's Flyspeck project to formalise the proof of his Kepler Conjecture proof) is much simpler than the rest, although the source code comments are rather sparse.

I released a new, open source HOL theorem prover last year, called HOL Zero. It fully implements the HOL logic, but is much simpler than the other systems (it only supports basic interaction, and is primarily aimed at checking proofs imported from other systems). I have gone to great lengths to make the source code and user interface as simple and easy to understand as possible, and the source code comments are very clear and extensive. Importantly, I have written a glossary that explains all the technical terminology used. So I recommend you take a look at HOL Zero if you want to get your hands dirty by looking at source code. If you want to actually run it, it requires OCaml (a dialect of ML) and a Unix-like operating system:

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

In my opinion, the main limitations of current systems are (in decreasing order of importance):

They take a long time to learn to use proficiently. It typically takes something like three to six months, and even then there is always more to learn.
Even when fairly proficient, you will inevitably occasionally (maybe once a day) come across infuriating situations where what appears to be the simplest of steps on paper takes an inordinate amount of interaction with the system (sometimes taking 10 minutes, sometimes hours).
They each have large gaps in their library of mathematical theory that has been established, so using them for serious work will inevitably involve developing a lot of supporting theory.
There is generally poor support for porting proofs between different systems.
When displaying results, each (except HOL Zero) suffers from problems that can occasionally mislead the user as to what has actually been proved.

Answer by Mark Adams for Why is it so difficult to write complete (computer verifiable) proofs?

2011-01-11T18:25:01Z

The problem of putting an existing mathematical proof through a theorem prover ("formalising a proof") breaks down into 3 inter-dependent stages (with an element of recursion between the stages). With the current state of the art, all three of these stages are agonising. This gets more difficult the larger the proof is.

The first stage is to re-express the proof in a sufficiently detailed, rigorous and coherent symbolic form (or "formalisable" form). Traditional mathematical proofs often switch between different underlying formalisms, and often without any mention that this is happening. Also, sometimes pictorial arguments may be used without any explicit symbolic justification. And there will typically be fairly big, unjustified steps (e.g. "it obviously follows that ...") that may be obvious to the expert in the field, but not immediately obvious to someone fairly new to the subject. All of this needs to be re-expressed. This stage is fundamentally difficult and software cannot really help much. I expect that over time this will become a little easier as people become more experienced. At the moment there are very few people in the world capable of doing this stage effectively for large proofs (perhaps just John Harrison, Tom Hales and Georges Gonthier).

The second stage is to fill in the gaps in the theorem prover's library for theory referenced in the formalisable proof. This involves giving definitions and proving properties in the theorem prover. Ideally the theory referenced will all fit together in a way that helps formalise the proof, and sometimes it will be necessary to come up with alternative formalisms of existing parts of the theorem prover's library. This is a very skilled job, but this stage will eventually become easier as bigger and better library support is built up for the theorem prover being used.

The third stage is to actually translate the formalisable proof into a script accepted by the theorem prover. Currently, this is also a very difficult stage. It will typically take several months to become adept at controlling a theorem prover, and even then some of the steps in the formalisable proof may be agonisingly difficult to achieve. A page of formalisable proof may take weeks to actually formalise. This stage, in my opinion, should be quick and easy for mathematicians, but it will take a small revolution in theorem prover usability to bring this about. I am currently working on this.

Answer by Mark Adams for Propositional Logic, First-Order Logic, and Higher-Order Logics

2011-01-29T08:43:11Z

Yes there are advantages/disadvantages in where the balance lies between the number of inference rules and the number of axioms when defining a logic. As Francois Dorais says in his answer, it depends on what you want to do with the logic.
All logics are for representing proofs, including propositional logic. The higher the order of the logic, the more powerful it is in the sense of its language being more expressive and its deduction being more general.
The criterion that determines the order of a logic relates to the kinds of value that can be quantified over. In a zeroth-order logic, there are just values and quantification is not supported (e.g. propositional logic, where the values are boolean values). In a first-order logic, there are functions which are distinct from values; only values can be quantified over (e.g. first-order predicate logic, natural number arithmetic). In a second-order logic, functions may take first-order functions as arguments, and first-order functions may be quantified over. In a third-order logic, second-order functions may themselves be arguments to functions and be quantified over, etc, etc. In a higher-order logic (this is a distinct concept from the concept of an nth-order logic), there is no fundamental distinction between functions and values, and all functions can be quantified over.

Note that usage of predicates can be considered as equivalent to usage of sets (some predicate returning "true" for a given value can be considered as equivalent to the value being an element of some set). Note also that a given logic may or may not fundamentally distinguish between general values and boolean values, and between functions and predicates (functions that return a boolean value).
Godel's (First) Incompleteness Theorem only relates to logics capable of at least expressing natural number arithmetic - any such logics are incomplete (unless they are inconsistent, in which case they are trivially complete). His Second Incompleteness Theorem relates to whether such logics are capable of proving their own consistency.

The advantage of a less powerful logic is that it is easier to reason about, and that it is tends to be easier to write algorithms for, in the sense that (depending on what the algorithm is intended to do) these algorithms will tend to be more complete and/or efficient and/or to terminate (e.g. algorithms for proving statements in the logic). The advantage of a more powerful logic is that it is more expressive and thus capable of representing and/or proving more of mathematics.

There are certainly higher-order logics that are not capable of expressing the whole of mathematics today (e.g. not capable of fully expressing category theory). I'm afraid I don't know enough to say whether there are/aren't any formal logics that are capable of expressing all of contemporary mathematics.
Type theory is the study of type systems. Presumably your question relates to the purpose of using a type system in a formal logic? (Apologies if I got the wrong end of the stick.)

Whether or not a logic uses a type system is another fundamental distinguishing attribute between logics. The alternative is to base the logic on set theory. Either way, the logic must somehow avoid consistency problems, like Russell's Paradox that exposed the inconsistency of Frege's formal logic, or the Kleene-Rosser Paradox that exposed the inconsistency of Church's original lambda calculus.

The purpose of a type system is to impose extra well-formedness restrictions on a formal language in addition to the restrictions imposed by the language's syntax. This is a way of ensuring that paradoxes can be avoided, as well as a practical way of helping the user of a logic avoid writing meaningless statements (such as "the number 5 is a vector space"). Russell actually invented type theory to solve the problem raised by his own paradox. Church used type theory to come up with an alternative, consistent lambda calculus.

Comment by Mark Adams

2011-09-21T11:45:08Z

@Sergei: I should add that there is an important philosophical distinction here between what is being achieved by proof auditing when trusting the parser and when trusting the printer. Trusting the parser establishes that the input is a formal proof of a given conjecture, whereas trusting the printer establishes that there exists a formal proof of a given conjecture. I'd argue that the latter is (normally) the pertinent issue. If the former is required, then, in practice, both the parser and printer need to be trusted.

Comment by Mark Adams

2011-09-21T11:30:03Z

@Sergei: I see. I agree that the language needs to be very well designed, and that this is crucial. Where we differ is whether it is the parser or the printer that we should trust (either is sufficient). I argue that it is better to concentrate on getting the printer right, because: 1. it is much easier for a human to audit the few pages of printer output that encapsulates the theorem prover state, rather than to audit the megabytes of proof checker input script; and 2. the auditor simply examines the results of what has executed, rather than trusting that parsed input gets correctly executed.

Comment by Mark Adams

2011-05-06T21:24:29Z

@joro: It depends on the kind of formal logic that it's for. There are various dedicated SAT solvers (for propositional logic only), many are dedicated to first-order logics (I understand that Vampire is supposed to be amongst the best), and then those for more expressive, higher-order logics (like HOL, Isabelle, Coq and PVS). In the hands of a sufficiently expert user, all the main "higher-end" systems can be used very effectively, but the trouble is there are only a handful of "sufficiently expert" users (and I am not one!). I'm afraid I don't know which are powerful but very easy to use.

Comment by Mark Adams

2011-05-06T15:41:51Z

Yes - and that's why we need "black-box" proof auditing, where you just examine the statement of the resulting proved theorem and the axioms used in its proof, and don't need to look at the 4GB proof script itself. But for this you need a theorem prover that you can trust to make sound deductions, record all axioms and print theorems correctly, with no dodgy architectural back-doors. There was no theorem prover that does all of these things, so I wrote the basic HOL Zero that does, for reading in proofs exported from more sophisticated systems so that they can be black-box proof audited.

Comment by Mark Adams

2011-05-06T05:50:49Z

@Andrej: Yes, we're largely agreeing. I think for everyday usage by mathematicians, the trustworthiness of LCF-style theorem provers like Coq, Isabelle, HOL Light, HOL4, etc is already perfectly acceptable (let's hope it stays that way). But for the most important applications, e.g. verifying critical software or reviewing mathematical journal submissions, some rigorous process of independently auditing a proof, to check that the right theorem has been proved, will be required; and having some sort of highly trustworthy auditing tool (or "anti malware"!) to support this would be very useful.

Comment by Mark Adams

2011-05-05T17:03:10Z

@joro: Ok so my reply is in a comment to your original question.

Comment by Mark Adams

2011-05-05T15:39:10Z

@joro: Yes, you'd get a reward if you could show |- true <=> false. See the HOL Zero webpage for more info and the download. It has no warranty (it has GPL3 licence), as is usual for all software I think. It would be somewhat foolhardy to give out free software and accept warranty! Be happy with $100!

Comment by Mark Adams

2011-05-05T10:57:04Z

@Joro: By the way, find something like this in my (admittedly very basic) theorem prover, HOL Zero, and you'll get a $100 reward!

Comment by Mark Adams

2011-05-05T10:52:33Z

... So with the right approach we can have the best of both worlds - safety and efficiency. Robin Milner's "LCF-style" architecture for theorem provers (used in Coq and other systems) was a massive leap in the right direction, greatly improving the trust we can put in systems. Unfortunately since then complacency about trust has pervaded theorem prover development. Observations like joro's should be taken very seriously, but sadly aren't.

Comment by Mark Adams

2011-05-05T10:38:54Z

@Andrej: I generally agree with the thrust of what you are saying - using theorem provers greatly improves mathematical rigour, and we can never be 100% certain. But we can do better than just accept that we must trust their users. With the right approach to building theorem provers, vulnerabilities can be effectively eliminated, regardless of whether the users are being trusted or not (although we still must do the human process of checking that the right theorem has been proved). This is especially useful if highly complex automated theorem prover routines are being used. ...

Comment by Mark Adams

2011-05-04T18:41:54Z

joro raises a valid vulnerability here, and should be congratulated on finding it. He also asks an extremely valid question about "assuming a dishonest human prover giving Coq proofs ...". If formal proof ever becomes really big, then there will be subcontractors paid to perform it, and realistically there will be some who will try to cheat. Equating such worries with the old chestnut about cosmic rays is sweeping this important issue under the carpet. But read my answer to the following: mathoverflow.net/questions/18421/…

Comment by Mark Adams

2011-05-04T18:28:38Z

It's good that the Coq FAQ has this list of 5 things that you trust when using Coq, but where in this list is the vulnerability highlighted above by joro? It's not really covered by the second item, "The Coq kernel implementation", because this only talks about mirroring the logic...

Comment by Mark Adams

2011-02-28T10:43:25Z

Could you explain how this relates to the question?

Comment by Mark Adams

2011-02-05T15:32:45Z

b) I'm not particularly familiar with semantics, but as I understand it semantics deals with values, or at least equivalences between values. The type system of a formal language would partition values in the semantics, forbidding equivalences between values of different type.

Comment by Mark Adams

2011-02-05T15:26:00Z

a) In higher-order logic, variables can range over any values. In nth-order logic there is explicit distinction between different kinds of variable, which must range over (n-1)th order values or lower. So in a logic dealing with natural numbers, a 0th-order value would be a natural number, a 1st-order value would be a function over natural numbers, e.g "+", a 2nd-order value is a function that takes function arguments, e.g. "IsBijection", etc. Higher-order logic does not necessarily imply use of type theory/category theory.