In the article “Formal proof—getting started” [2007a], Freek Wiedijk introduces the practical use of formal proof assistants. He shows how two contrasting programs, Mizar and HOL Light, can be used to formalise and check an elementary number theoretic proof of the Law of Quadratic Reciprocity. Mizar has a declarative proof style, whilst HOL Light is a procedural system. In this post and the next, I’ll work through Wiedijk’s [2007a] approach and include a few details about Mizar and HOL Light along the way.
1. Principles of Mizar
First let us briefly cover some basic principles of mathematical formalization and proof verification in Mizar. We essentially summarise parts of the following references: Wiedijk “Writing a Mizar article in nine easy steps” [2007b]; Grabowski, Kornilowicz, & Naumowicz “Mizar in a Nutshell” [2010]; the Mizar wiki; and the Mizar home page. These are all good resources for further details on Mizar.
The Mizar system is built on the axioms of Tarski–Grothendieck set theory, an extension of ZFC. Getting to grips with Mizar’s syntax in order to formalise a proof requires a little background in first order predicate calculus. Even the basic concept of a natural number is used in no less than three syntactically different ways in Mizar (Wiedijk [2007b] p. 12): “NAT” is a term referring to the set of natural numbers; “Nat” is a type of element; “natural” is an adjective. But what are terms, types and adjectives in Mizar? How do we combine them to describe a concept such as “let A be a subset of the natural numbers”?
The following are some core principles of Mizar’s syntax, summarized from Wiedijk [2007b]:
(1.1) Everything is an operator.
In Mizar, unlike most programming languages, there is no syntactical distinction between function notation and operator notation. For example, “x+y” and “f(x,y)” are syntactically the same thing: in “f(x,y)”, symbol “f” is simply a binary postfix operator.
(1.2) Predicate logic formulas are straightforward.
Logical connectives and quantifiers are translated into Mizar in an intuitive way. For example, the logical connective and has the symbol “&” and the quantifier exists x such that… is symbolized by “ex x st…”. Mizar formalisations are therefore somewhat readable, like standard mathematics. A useful table of standard connetives is found in Grabowski et al. [2010], p. 155. Keep the order of precedence of the logical operators in mind!
(1.3) Mizar is a typed language.
Every single variable in a Mizar formula must be assigned a type. There are two ways to do this:
(i) Attribute the type within a formula, using the “being” attribution, e.g.:
“ex m, n being Nat st…”
(ii) Attribute the type before the formula, using a “reserve” statement, e.g.:
“reserve m,n for Nat; ex m,n st…”
(This latter is useful when several statements are written with the same type of variables.)
(1.4) How to write atomic formulas in Mizar.
An atomic formula consists of terms connected by zero or more predicate symbols and no logical connectives. Again, there are two ways to construct atomic formulas in Mizar:
(i) With a predicate (relational) symbol R:
“x1, …, xm R xm+1, …, xm+n”
A short list of common relations is found in Wiedijk [2007b], p. 8. (Note that brackets are not allowed around the arguments of the predicate.)
(ii) If T is a type or an adjective part of a type, we can write a type judgement (see point 1.7 below): “x is T”.
(1.5) How to write terms in Mizar.
Intuitively, a term is an object in the formal language. In Mizar, there are three ways to write terms:
(i) Using an operator symbol “f”:
“(x1, …, xm) f (xm+1, …, xm+n)”
A list of common operators is found in Wiedijk [2007b], p. 9.
(ii) For left and right bracket symbols L and R: “L x1, …, xn R”
(iii) Any natural number is a Mizar term.
(1.6) A function in the set theory is different to a function in the language.
It is good to bear in mind the difference between a function application within the axiomatic set theory on which Mizar is built, and the application of a functor operator in the programming language. If “f” is a function in the set theory, that is, a set of ordered pairs, then “f.x” (using the ” . ” operator) gives the image of element x under “f”. But if “f” is a symbol in the language, representing, for example, a function with zero left arguments and one right argument, then we use “fx” or “f(x)” to create the necessary term (see point 1.5(i)).
(1.7) Types consist of modes preceded by adjectives.
The basis of a mizar type is a mode. Each mode takes a certain number of arguments (terms); this is part of the definition of each mode. The keyword “of” binds any arguments to the mode. For example, the mode “Subset” has one argument, and so we can write “Subset of NAT”. Modes have a cluster of adjectives in front. Adjectives are either an attribute, such as “empty” or “finite”, or the negation of an attribute using the keyword “non”. So we can write “non empty finite Subset of NAT”; this is an example of a Mizar type. Modes themselves are dependent types, and modes depend on terms.
In Mizar, types are used in declarations, for example, “n be Nat”. In this case, keywords “be” and “being” go between a variable (“n”) and a type (“Nat”). Types are also used in type judgement formulas in the logic. For example, the keyword “is” goes between a term and type or a term and an adjective e.g. “n is Nat” or “n is natural”, respectively (see point 1.4(ii)).
(1.8) Automatic quantification of free variables.
Mizar implicitly quantifies over free variables which have appeared in a “reserve” statement, with a “for all” quantifier.
2. Mizar articles
A formalized Mizar proof is contained in a text file called an article, which has extension “.miz”. Articles are verified either on the command line, using the command “mizf “, or in emacs with Mizar mode, by hitting C-c RET. An article consists of two sections:
“environ
…
begin
…”
The formalized proof is written in under “begin”. A discussion of Mizar’s verification process in detail is beyond the scope of the present article: essentially, a formalized proof is valid if each step can be justified either by basic logical argument or by citing a previously verified proof. A theorem in the Mizar article is proved according to the following structure:
“statement
proof
proof steps
end;”
The goal, or thesis, of the proof is the statement that needs to be proved. A proof consists of proof steps. Some steps, called skeleton steps, reduce the thesis. By the “end” point of the proof, the thesis should be reduced to the Top symbol, otherwise you will get a *70 error: something remains to be proved. The four basic skeleton proof steps are assume, thus, let, and take; for examples on how they are used, see Wiedijk [2007b], p. 28. Other frequently used proof steps are compact, consider, per cases/suppose, set, reconsider, and iterative equality (a chain of equalities). An advantage of Mizar is that the nature of these steps can be guessed from their names, improving the readability of the formalizations.
All the proof steps must be justified for the proof to be complete. There are three ways to do this:
1. Simply putting ‘;’ after the statement: “statement;”, if Mizar can prove it by itself.
2. Putting the justifier “by” after the statement, followed by a list of labels of previous statements or other named Mizar articles that it follows from:
“statement by reference1, …, referencek;”
3. Using a nested subproof:
“statement
proof
steps in the subproof
end;”
Detailed explanations of the many proof patterns in Mizar can be found in Grabowski et al. [2010], Section 2.2.
As mentioned previously, Mizar is based on predicate logic with Tarski-Grothendieck set theory, which (loosely speaking) is ZFC additionally with Tarski’s Aziom. Mizar proofs often depend heavily on previous results held in the Mizar Mathematical Library (the MML – more on that below). In order to import what you need from the MML into your article, the correct environment must be set up. This is done by adding directives in the “environ” section of the article, a process which can be quite complicated as you search for what you need in the MML. Directives are usually vocabularies, notations and constructors, each of which supply different types of information about the objects used in the proof. If you refer to another theorem in your proof, the article for that theorem should be under a theorems directive.
The Mizar Mathematical Library (MML) is currently the largest repository of formalized mathematics. If and when a theorem is verified by Mizar and evaluated for style and content by peer-review, then it will be published in the Journal of Formalized Mathematics and added to the MML. The MML can be difficult to search due to its large size. A wiki version of the MML exists. The MML can also be queried via the MML Query website.
Now that we have a (very) basic handle on how Mizar works, we will go ahead and look at the formalization of the law of quadratic reciprocity in Mizar.
3. The law of quadratic reciprocity
For distinct odd primes p and q, the law of quadratic reciprocity (which I will call QR for short) links whether p is a quadratic residue modulo q to whether q is a quadratic residue modulo p. Following incomplete attemps by Euler and Legendre, QR was first proven by Gauss who referred to it as the “fundamental theorem”, writing that “the fundamental theorem must certainly be regarded as one of the most elegant of its type”. There are now more than 200 different published proofs of QR. We will take a superficial overview of an elementary number theoretic proof, based on Gauss’ third proof. This proof has been formalised with Mizar and HOL Light proof assistants, as summarized in Wiedijk [2007a] . Additional details are taken from Burton’s Elementary Number Theory (Ed. 6), Chapter 9. (For a step-by-step guide to the full proof, see Chapter 9 of Burton’s book.)
An integer a is a quadratic residue modulo p if it is congruent to a perfect square modulo p, in other words, there exists some x such that x2 is congruent to a modulo p. For a such that for odd prime p, gcd(a,p) = 1, Legendre introduced the symbol (a|p) (not to be confused with a fraction or the division symbol), defined by: (a|p) = 1 if a is a quadratic residue modulo p and (a|p) = -1 if a is not a quadratic residue modulo p.
The law of quadratic reciprocity states that if p, q are distinct odd primes, then
(p|q).(q|p) = (-1)((p-1)/2).((q-1)/2). Clearly ((p-1)/2).((q-1)/2) is even if and only if at least one of p, q is of the form 4k + 1. Thus QR states that (p|q) and (q|p) have the same value unless both p and q are of the form 4k+ 3, in which case (p|q) and (q|p) have opposite values.
The first thing to do is to establish Euler’s criterion: for odd prime p and integer a such that gcd(a,p) = 1, a is a quadratic residue of p if and only if a(p-1)/2 is congruent to 1 mod p; otherwise, a(p-1)/2 is congruent to -1 mod p. Most proofs of QR then use Euler’s criterion to prove Gauss’ lemma: for a and p as above, let n denote the number of integers that are in the set S = {ka: 1 
(p/q).(q/p) = (-1)n. (-1)m (from Gauss’ lemma)
= (-1)(n+m)
= (-1)((p-1)/2).((q-1)/2).
4. The law of quadratic reciprocity formalized in Mizar
The proof of the law of quadratic reciprocity, along with a proof of Gauss’ lemma, is held (at time of writing) in MML article INT_5 (int_5.miz). Now, different versions (installations) of Mizar need to use different versions of the INT_5 article. The required version can be found in the MML directory that is copied in along with the Mizar installation, in $MIZFILES/mml/int_5.miz. A further abstract file, containing a summary of all theorems and lemmas that are to be proved in the article, can be found at $MIZFILES/abstr/int_5.abs. At the time of writing, I am using Mizar Version 8.1.02 (Darwin/FPC) installed on Mac OS X 10.8.5. Due to incremental updates and changes since 2007 to the MML and Mizar software itself, the version of INT_5 linked to within Wiedijk [2007a] (ref 12) won’t run without error on more recent releases of Mizar.
It is interesting to explore whether the Mizar checker notices new edits to the proof which make the proof incorrect. To take one example, what happens if we change the definition of the Legendre symbol (Def3) such that (a|p) = 2, instead of 1, when a is a quadratic residue modulo p? Surely that would mess up the entire proof of the QR as the final result would no longer hold in general. However, “mizf text/int_5.miz” still runs without an error message on the command line. Does that mean that the checker missed this erroneous edit? On opening the file, the answer is no: there is a new error message *4 this inference is not accepted in the lemma immediately following the definition (Th25):
“theorem Th25:
Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = -1
proof
per cases;
suppose a is_quadratic_residue_mod p & a mod p <> 0;
hence thesis by Def3;
::> *4”
This makes sense, because now when a is a quadratic residue modulo p, (a|p) = 2, which is none of 1, 0, or -1.
Finally, Wiedijk [2007a], p. 11, asks us to look at the 11th lemma (Th11), whose statement as quoted in the paper is:
i gcd m = 1 & i is_quadratic_residue_mod m & i,j are_congruent_mod m implies j is_quadratic_residue_mod m
and decide whether condition “i gcd m = 1” is used in the proof of the lemma, for example by testing whether removing it affects the checking of the proof. However, this condition is not necessary for proving a general form of the lemma to be true, and someone must have already incorporated this change in subsequent edits to the INT_5 article, as a more general form of the lemma is now used instead (without that particular condition present)!
5. Conclusions
Mizar takes an intuitive approach to formalizing mathematical proofs. Writing (or merely reading) a Mizar article brings home how, in standard mathematical proofs, the numerous shared assumptions between writer and reader allow proofs to be much shorter than a full formalisation requires. Running article INT_5 for the law of quadratic reciprocity illustrates how Mizar highlights any errors introduced to the proof. However, the fact that a particular version of an article only runs in a particular Mizar version/environment reveals the difficulty of maintaining a huge library of theorem formalisations such as the MML. The inevitable changes and updates that accrue within the library and the Mizar software, such as re-defitions of concepts, renamings of files, or improvements to how Mizar verifies proof steps, can quickly render older articles to be full of “errors” that must be updated in order to run with the newest Mizar versions.
We also find that the “mizf” command may run without spitting out an error message on the command line even if the formalised proof is not correct, as we see above in the situation where changes to definitions in the proof were made that rendered the following arguments invalid. After Mizar-ing, we must always check the end of the article text file for any new error messages that may be printed there, rather than on the command line.
In a later article, still following Wiedijk [2007a], I’ll explore how the law of quadratic reciprocity may be formalized in a very different proof assistant: HOL Light.
REFERENCES
Burton D. M. Elementary Number Theory. McGraw-Hill, (6th Ed., 2007).
Grabowski, A., Kornilowicz, A., & Naumowicz, A. Mizar in a Nutshell. Jounral of Formalized Reasoning, Vol. 3, No. 22, pp. 153-245. 2010.
Mizar home page: http://www.mizar.org
Mizar Mathematical Library (MML) wiki: http://mws.cs.ru.nl/mwiki/
Mizar Wiki: http://wiki.mizar.org/twiki/bin/view/Mizar/WebHome
Wiedijk, F. Formal proof – getting started. Notices of the AMS, Vol. 55, No. 1, pp. 1408-1414. 2007a.
Wiedijk, F. Writing a Mizar article in nine easy steps. 2007b. http://www.cs.ru.nl/ ̃freek/mizar/mizman.pdf