Examples of new mathematics discovered through formalization?

Question

In his essay Why formalize mathematics?, Patrick Massot discusses several reasons behind why a working mathematician might be interested in proof formalization. One of the the reasons he discusses is, perhaps somewhat counterintuitively, that working within a proof assistant can actually help create new mathematics, not just write up proofs of existing results. Unfortunately, currently working on formalizations tends to be a slow down more so than a helpful tool, and to quote Massot, "getting such help to create new theorems is mostly science fiction with current day technology".

Nevertheless, the methodical way in which proof assitants work can still be a sort of aid when trying to work on mathematics. What are some examples of such "success stories" in which formalization efforts have lead to new mathematical discoveries?

Answer 1

One quite concrete example of this is discussed by Massot in the essay linked in the original post. During the work on the Liquid Tensor Experiment (formalizing the proof of a theorem due to Scholze in his analytic geometry), the formalization effort has helped isolate the properties of the Breen-Deligne complex required for the proof. Existence of Breen-Deligne resolutions is a rather difficult and inexplicit result relying on ideas from stable homotopy theory, but Johan Commelin has constructed a simpler and much more explicit resolution which can be used in its place.

You can find some more details in this post, including a remark of Scholze that this new resolution might play an important role in future work.

Answer 2

As David Roberts mentioned in a comment, this happens relatively frequently in the field of homotopy type theory / univalent foundations. Often in that area (at least, in my experience), a proof-assistant formalization is part and parcel of developing mathematics in the first place, and then only afterwards is the formalized proof written down in mathematical English. This is mentioned in the HoTT Book, and applies particularly to the results in Chapter 8 (synthetic homotopy theory). If you want a specific example, the first concrete calculation in synthetic homotopy theory -- the proof that the fundamental group of the circle is the integers -- was invented using Coq and only afterwards extracted into a blog post and a paper.

One reason for this is that many of the proofs in HoTT/UF, particularly synthetic homotopy theory, are "closer to the metal" of the formal systems (dependent type theory) that proof assistants are based on. On one, hand, this means that dealing with the idiosyncracies of those systems, which can seem more like "bureaucracy" or "engineering" that part of the "real proof" in other situations, really is more at the core of the mathematical activity. It also means that formalization is easier than in many other cases, at least in the sense of being "narrower" (if perhaps "deeper").

Another reason for this is that we are still developing intuitions for HoTT/UF and deciding how to do this sort of mathematics informally. As a foundation for mathematics, it's different enough that (at least when working with more novel features like synthetic homotopy theory) it's easy to make real mistakes when working on paper, and a proof assistant can help catch them. A proof assistant can also help develop one's intuition, by giving realtime feedback about what is and isn't allowed.

David's comment expressed some doubt about whether this counts as "new mathematics". I think that it inarguably does. It's not just giving new proofs of old results; it really is proving new theorems. It's true that theorems with the same one-line description, like "the fundamental group of the circle is the integers", are already known in classical mathematics; but the theorem is different because the meaning of the words is different, including "fundamental group", "circle", "integers", and even "is". There is an interpretation of HoTT/UF into classical mathematics using the simplicial set model, which means that the HoTT/UF theorem implies the classical theorem (and thereby gives a new proof of it), but the HoTT/UF theorem says more than this.

Answer 3

Not new in an absolute sense, but when formalizing my recent paper the formalization process lead me to discover for myself the formula $$f(A,B,C)=f(C,B,A)$$ where $$f(A,B,C)=|A\setminus B|+|B\setminus C|+|C\setminus A|$$ and $|A|$ is the cardinality of the finite set $A$. Using this formula in the proof made it less painful to formalize.