Foreword to: Special Issue on Interactive Theorem Provers

Here at Experimental Mathematics, we like to live up to our moniker. One of the seemingly major innovations in recent times is the rapid expansion of the capabilities of software for formalizing mathematics in interactive theorem provers, to the point that certain papers in top journals can be proved formally about a year or so after the appearance of their “human” versions. The goal of this Special Issue is to record the current state-of-the-art in formalization, and to understand the potential impact such software may have on research mathematics in the near to mid-term future.

It certainly seems plausible that 20 years from now, there will exist very highly regarded journals which will only accept formalized proofs. Some of the more committed proselytizers argue that all of the top journals will switch, if not in 20 years, then in 50. (This is not as radical a claim as it may first seem, nor would such a transition be all that unusual in mathematics; e.g., presumably there was a point in the 19th century when it became required for research papers in calculus to include “rigorous” proofs using Cauchy’s ε/δ formalism. From Newton to the Bernoullis to Euler’s nearly thousand publications, no ε’s or δ’s were harmed.)

This is particularly interesting from the viewpoint of what it may mean for the publishing process, which currently suffers from a number of inefficiencies. The first of these is error detection and correction. It is common these days to send out first for “quick opinions” of the form: assuming the results are correct, would the main theorems be of sufficient novelty and importance to warrant publication in such-and- such selective journal. If these reports (often from senior, seasoned experts, and usually returned within a month or two) are positive, then an editor has the much more daunting task of securing referees willing to go through the paper with a fine-toothed comb and check, as best they can, for mathematical errors. (In practice, these are frequently more junior researchers, who may both have fewer other service-type obligations occupying their time, and may also stand to gain valuable experience from reading the submitted paper extremely thoroughly.) Naturally, some of the most important results are also the most difficult to verify, and prone to errors which are not discovered at the refereeing stage. Instances of such abound, so we will not repeat them here.

Beyond error correction, submission of formalized mathematics may allow for a much more rapid refereeing process, in which one may need only check that the definitions and theorems have been formalized correctly (which in and of itself is a rather subtle, nontrivial task!), and then let the compiler do the rest.¹ Indeed, this is largely how this Special Issue was assembled: referees had plenty of comments on the exposition and quality of results submitted, as well as in some cases correcting the very definitions being formalized, but beyond that, everything was up to the code compiling, allowing for a minimal delay from submission to a decision. It will be rather interesting to see the creation of new journals following such models in the near future. Currently most of the formalized research mathematics is being recorded in computer science journals and conference proceedings; if the pure mathematics community wishes to see the promises of formalization come to fruition, we must work to create respected journals within mathematics itself, to give proper credit for this work in ways that will be familiar to our current standards of evaluation.

We now give a few words about the present volume of which the first 80 or so pages are devoted to the topic of the Special Issue. We begin with Peter Scholze’s challenge to the formalization community to verify his work with Dustin Clausen on so-called condensed mathematics. As has been recorded elsewhere (see, e.g., (1)) the “mathlib” community using the Lean interactive theorem prover took up the challenge, and within six months was able to complete the most arduous (and precarious) aspects of the proof, showcasing that, indeed, such technology is fully capable of formalizing some of the most difficult modern research. It is rather remarkable that the solution to Scholze’s challenge could be completed before even the challenge’s publication in the present volume! (That said, as of this writing, Lean has only the most preliminary understanding of undergraduate Complex Analysis.)

Next are two papers on formalizations of schemes using different formalization platforms, one in Lean, and one in Isabelle; it is interesting to read the two accounts side by side and compare and contrast their approaches and difficulties encountered. These are followed by three papers on theorems in: (i) ordinal partition relations, (ii) criteria for irrationality and/or transcendence of certain infinite series, and (iii) Galois theory, formalized in Isabelle, Isabelle, and Lean, respectively; these showcase some of the variety of mathematics currently amenable to formalization.

Again, this Special Issue serves as but a snapshot of the state of affairs in the present capabilities of interactive theorem provers. Time will tell whether these experiments will succeed in bringing about the revolutions in research mathematics their progenitors envision.

Alex Kontorovich
Editor-in-Chief, Experimental Mathematics
Professor of Mathematics, Rutgers University
[email protected]

Notes

1 Of course then one must be confident in the accuracy of the compiler, but most people seem to agree that whatever errors it may introduce will be far fewer than the track record of our current human process.