Towards a standard file format for formal sketches of mathematical articles

The large-scale formalization of mathematics has been a long-time dream of many. Personally, I would love to accompany every mathematical research article I write with a formal version, including formal proofs, and I think widespread formalization is important for the mathematical community in general.

However, as long as current automatic proof systems are unable to do even high school mathematics on their own, this dream will not turn into reality. Yet, we do not need to wait for automatic proof systems to get better. On the contrary, there is something that we can do now that will help both the formalization of mathematics and the improvement of automatic proof systems:

We need to create a standard file format for formal sketches of mathematical articles.

In the rest of this post, I will explain what I mean by this and why I think this is useful. Note, however, that these ideas are very much a work in progress. Also, I should say that my perspective is that of a mathematician working in discrete geometry and combinatorics. I am not a logician and I am no expert in interactive or automatic theorem proving, and I have begun to explore the world of formal proof systems only recently. Nonetheless, I think that the one thing that could make writing formal mathematical proofs more accessible to a working mathematician like me is a standard file format for formal sketches of mathematical articles.

Formal Sketches

With a mathematical article I mean an informal mathematical article on some topic of current research interest, as might be found in a journal or on the arXiv. With a formal sketch I mean a formal version of such an informal mathematical article with the following properties:

A formal sketch contains the definitions, theorems and proofs given in the informal mathematical article.
The formal sketch is human-readable and human-writable.
Moreover, reading or writing a formal sketch of an informal mathematical article should not be significantly more difficult than reading or writing the informal article itself.
Definitions and theorems in the formal sketch are given in a fixed logic without any ambiguity.
Proofs in the formal sketch are formal proof sketches in the following sense: A formal proof sketch is not a complete formal proof and it is not a human readable representation of a given formal proof. Instead, a formal proof sketch serves as advice for constructing a formal proof by breaking the task of constructing a formal proof down into smaller, easier steps. The purpose of a formal proof sketch is to help an automatic proof system to construct a complete formal proof.
Formal proof sketches are independent of any particular automatic proof system and any fixed library of definitions and theorems. Formal sketches of mathematical articles follow a decentralized open-world approach to formalizing mathematical theory.

I do not claim that current automatic proof systems will actually be able to construct a formal proof from a formal proof sketch. This goal may still be many years away. Current automatic proof systems will still require additional prover-specific human help to construct formal proofs. Nonetheless, I argue that it is still beneficial to create a standard file format for formal proof sketches now.

The creation of a standard file format for formal sketches of mathematical articles will, I hope, accomplish two things:

A standard file format for formal sketches of mathematical articles will make it more attractive for everyday mathematicians to formalize their mathematical articles. This will facilitate the creation of a large body of formalized real-world mathematics. Moreover, this effect will become more pronounced as automatic proof systems become more powerful.
A standard file format for formal sketches of mathematical articles will encourage competition between automatic theorem provers and innovation in automated reasoning. Formal sketches may serve as a benchmark for comparing the capabilities of different provers. The availability of an interesting set of formal proof sketches will also make improvements in the automated reasoning capabilities of current provers more relevant.

These two effects mutually reinforce each other. This has the potential to create a positive feedback loop that will help the large scale formalization of mathematics to take off, finally.

Of course, a large effort will be required to get this process going. One means of bootstrapping this process may be the creation of a supplemental file format for the annotation of formal proof sketches with prover-specific advice. Nonetheless, I think that the creation of such an ecosystem is possible and that the potential benefits justify the effort. As outlined above, the foundation of this system is a standard file format for formal sketches of mathematical articles.

In the remainder of this post I will discuss how such a standard file format might look like.

What file formats are out there already?

Fortunately, there is already a rough consensus on what a formal, human-readable, declarative language that resembles ordinary mathematics should look like. Many people tried to come up with their own version of such a language and, independently, they arrived at essentially the same result, a common mathematical vernacular. This argument has been made by Freek Wiedijk in a wonderful article where he compares the languages of the Hyperproof, Mizar and Isabelle/Isar systems and points out the common structure behind their differences in surface syntax. His miz3 syntax for HOL Light is another example of this mathematical vernacular.

This mathematical vernacular is a format for formal proofs with a very precise meaning. Formal sketches, on the other hand, should live at a higher level of abstraction. In particular they should be intentionally vague in specifying how, exactly, to prove “the next step” in a declarative proof. Freek has introduced the notion of a formal proof sketch and given some very nice examples. A formal proof sketch, in his sense, is an abbreviated version of a full formal proof in the Mizar language, in which some intermediate steps and justifications have been removed. It turns out that using such abbreviations, one can arrive at a document that is very close to a natural language version of the proof and that still accurately reflects the structure of the underlying formal proof. A formal proof sketch is correct if it can be extended to a formal proof in the Mizar language just by adding labels, justifications and intermediate steps.

Freek intends formal proof sketches to serve only as a means for presenting a formal proof. He expressly does not intend formal proof sketches “to be a ‘better way’ of writing formal proofs”. In this post, however, I use the terms “formal sketch” and “formal proof sketch” with the explicit intent of employing these sketches as a tool for authoring and archiving formal proofs.

In the context of this prior work, a formal sketch in the sense of this post would be the following: A document containing definitions, theorems and proofs, where the proofs are written in an abbreviated version of the mathematical vernacular. Such a document would be correct, if the proofs can be extended to full formal proofs in the mathematical vernacular by adding labels, intermediate steps and additional justifications. Such a formal document would not serve as an abbreviated representation of an underlying formal proof. Rather, it would serve as formal but ambiguous and incomplete advice to the (human or machine) reader for constructing a formal proof.

The purpose of creating a standard file format for formal sketches based on the mathematical vernacular is to share formal sketches across different proof systems. In this regard, the OpenTheory project has done vital pioneering work. The OpenTheory article format is a low-level format for encoding proofs in a fixed logic. This file format can be read, written and interpreted by several different provers. The OpenTheory article format is prover independent in the sense that in order to use the proofs contained in an OpenTheory article, a prover only has to use a version of higher order logic that can simulate the primitive inference rules defined in the OpenTheory article standard. OpenTheory demonstrates that sharing of proof documents among provers is possible. The creation of a standard for formal sketches of mathematical articles would aim to do the same at higher level of abstraction.

OpenTheory achieves prover independence by compiling prover-specific proof tactics down to elementary inferences. The only way to achieve prover independence at the high level of abstraction that formal sketches aim for, is by removing all prover-specific tactics and library-specific references from the justifications of the declarative proof steps. (Incidentally, this removal of justifications is also Freek’s key step in converting a declarative formal proof into a formal proof sketch.) In this way, the higher level of abstraction is “bought” at the cost of introducing ambiguities into the formal proof sketch.

In terms of previous work, a standard for formal sketches of mathematical articles could thus be described by the slogan “OpenTheory for formal sketches of Mizar-style articles”. In the next section, however, I want to change tack and describe the properties a format for formal sketches should have, by drawing analogies to informal mathematical articles as they are used today. In particular, I will argue that informal mathematical articles are successful precisely because they are ambiguous.

What properties should the file format have?

The research articles that mathematicians all over the world write every day have several astonishing properties. Compared to most other texts humans write, even in the sciences, mathematical articles are extremely formal. Yet, compared to formal proofs in the sense of proof theory, mathematical articles are extremely informal, ambiguous, imprecise and even erroneous. There are three aspects of this inherent ambiguity of mathematical articles that I want to call particular attention to.

Even though mathematical articles build on a huge amount of previous results, they manage to refer to this huge body of knowledge without becoming too verbose. This feat is achieved by three means: Mathematical articles typically 1) assume background knowledge on part of the reader, 2) include brief preliminary sections that summarize the most important parts of the required background knowledge, and 3) state the most important previous results they draw on as explicit theorems.
Mathematical proofs are written in a declarative rather than in a procedural style. They consist of a sequence of true assertions, rather than a sequence of instructions on how exactly to get from one assertion to the next. This allows readers to make use of their own background knowledge and understanding of the subject matter and avoids a commitment to any particular set of rules.
To make sense of a mathematical article in all its details requires an often significant effort on the part of the reader. Every mathematician has been in the situation of spending hours trying to understand a step in a proof that was (apparently) obvious to the author. This is made necessary by the previous two properties of mathematical articles mentioned above.

All three of these properties make mathematical articles more successful at communicating mathematical ideas. Mathematical articles would be less readable today and completely unintelligible 50 years from now, if they were extremely verbose, required the reader to refer to a particular textbook while reading and forced the reader to follow exactly the same train of thought the author used.

I think there is something we can learn from this:

Mathematical articles have been successful at communicating mathematics in the last centuries precisely because they are ambiguous. Formal mathematical articles have to embrace this ambiguity if they are to become successful.

Concretely, this has the following implications for a formal format for mathematical articles.

Formal mathematical articles have to avoid binding themselves to any particular library of theorems or any particular proof system.
Formal mathematical articles should be written in a declarative style.
Formal mathematical articles have to place the burden of working out the details on the reader, no matter if the reader is a human or an automatic proof system.

These general considerations point to a declarative format for formal proof sketches in the Mizar style in which the explicit references to external theorems and prover specific tactics have been removed as far as possible.

From a pragmatic point of view, the removal of most explicit references to libraries and provers from formal sketches has two huge advantages for mathematicians wanting to formalize their articles:

Mathematicians do not have to learn a (huge) dictionary or “API” to get started with formalization.
Mathematicians do not have to fear that their formal sketches will become unreadable when the current generation of provers becomes obsolete.

These two factors, the tie-in and the steeper learning curve associated with binding a formal sketch to a particular API, are the two factors that keep me personally, as an everyday mathematician, from starting to formalize my research. (The danger that formal proofs break as prover technology changes is particularly problematic.) The removal of these two deterrents would, I hope, make formalization attractive to many other mathematicians as well.

The ingredients of a specification

So far, these are blue-sky ideas and it is way to early to try to turn these into an explicit specification of a formal sketch format (FSF). But, to get the ball rolling, I want to list some ingredients for such a specification that, I think, will be important for success, based on the above considerations.

As explained above, the starting point for FSF is a Mizar-style declarative proof language in the spirit of the mathematical vernacular. Proofs in FSF are abbreviated by omitting intermediate steps and in particular justifications. Prover-specific justifications are not allowed in formal sketches at all. To make FSF work, this basic concept should be extended in the following ways.

First of all, as this whole idea revolves about creating a cross-prover file format, close integration with OpenTheory is desirable. In particular:

FSF should use the same logical foundation as OpenTheory.
The packaging mechanism should be essentially the same as in OpenTheory. An FSF article imports theorems as axioms and promises to produce a bunch of new theorems as a result (if the reader/prover is clever enough). Note that while the set of exports is uniquely determined by the FSF article, the set of imports is not uniquely determined by the FSF article, but depends on the reader/prover as well.
The benchmark for whether a prover $P$ “understands” formal sketch $S$ should be this: Is $P$ able to transform $S$ into an OpenTheory article $O$ on its own? $O$ is not uniquely determined by $S$, in particular its imports may depend on $P$. However, all imports of $O$ should be available in $P$’s library.
FSF should have built-in support for citing theorems from the OpenTheory library.

The formal sketch format should not tie itself to OpenTheory exclusively, however, as independence of any particular system is crucial for the success of FSF. Instead:

FSF has to embrace an open-world model.
FSF has to allow all kinds of references to mathematics outside of a given formal sketch article, including references to theorems that are ambiguous or not machine-readable. Examples include:
- informal citations of an informal mathematical source, like “Proposition 2.1 in Herbert Wilf, generatingfunctionology, 3rd Edition”,
- explicitly stated theorems,
- references to open libraries such as Isabelle’s Archive of Formal Proofs, and even
- free format URLs.

It is important to note that automatic systems processing FSF should not be required to make sense of any of these. A mathematician does not check all references cited in a given article either.

As mentioned before, current provers will probably not be able to “understand” any interesting formal sketch at this time. While the hope is that provers will achieve that goal at least for some formal sketches in the not too distant future, there is definitely going to be a transition period in which provers need additional advice to cope with a given formal sketch. To this end, a supplemental file format for annotating FSF articles should be developed.

An annotation file $A$ for an FSF article $S$ will consist of prover-specific advice for some steps of the proofs contained in $S$.
There can be many annotation files for any given article $S$. Different annotation files may give contradictory proof advice.
It is important that annotations reside in different files than the sketch $S$ itself, so that annotations may be changed, extended or removed while keeping $S$ fixed. Also, this prevents $S$ from becoming unnecessarily verbose.
As explained above, FSF articles should have explicit justifications only in places where humans would mention these justifications in informal mathematical articles. However, independently of the number of justifications, FSF articles can be made easier for provers to “understand” if they contain many small intermediate steps. While these small steps may be very useful in early FSF articles, they pose the danger of making an FSF article less readable for humans. Therefore:
- It should be possible to move these “small steps” into annotation files.
- In the case that these “small steps” are kept in the formal sketch itself, the file format should contain hints indicating which parts of a proof should be “hidden” or “folded” at a first reading.

The goal is of course to progressively remove annotations as provers become more powerful, until the annotations can be omitted entirely.

People tend to have very strong opinions about the surface syntax of any data format. As Freek pointed out, even the different variations of Mizar-style file formats that are out there attach different meanings to the same keywords. Therefore:

The FSF specification should fix one data model for formal sketches.
FSF should allow for different serialization formats of this data model.
The FSF specification should provide at least two different serialization formats:
- a Mizar-style plain text serialization for human editing, and
- a plain text serialization that lends itself to easy machine processing (using JSON, XML or Lisp-style S-expressions).

The formal sketch format needs to be supported by a convenient infrastructure. In particular, it will be useful to create

an open repository for formal proof sketches, and
standard interfaces for processing a proof sketch plus annotations with the most popular provers.

One might even imagine facilities to “mix-and-match” provers: Use HOL to do the first step in a proof, use Isabelle for the second and have both produce low-level output in OpenTheory format in the process. But of course the realization of such fancy ideas is even further off than a basic version of FSF. Which brings me to the conclusion of this post.

Next steps

Where to go from here? Before trying to go for a formal specification, a proof-of-concept is needed. Therefore, I plan to do the following:

Create a rough draft of a formal sketch format and an accompanying format for annotations.
Convert a couple of Freek’s formal proof sketches into this formal sketch format.
Implement a basic interface for compiling the example sketches plus annotations into OpenTheory articles - for two different provers.
Create annotations so that the formal proof sketches actually compile with these two different provers.
Begin experiments on how the provers in question can be improved to do these same proofs with fewer annotations.

At that point, we will have a clearer idea of how the formal sketch format should look and what needs to be done to get this positive feedback loop of more prover-independent formalized mathematics and more powerful automatic provers going.

Comments on these ideas and help in this process are very welcome!