25
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ I think in the course of formalizing the Kepler conjecture Tom Hales discovered a new theorem related to sphere packing. (Of course one could argument that if you stare at any theorem for 10 years, you will find something new. :)) If someone knows the details, they can post it as an answer. $\endgroup$
    – Jason Rute
    Feb 9, 2022 at 3:49
  • $\begingroup$ I'm trying to recall instances in the UF/HoTT special year (or its immediate aftermath) whereby proofs were first done in a proof assistant, then de-formalised for writing down in TeX. Not sure this counts as "new mathematics", but definitely there were new proofs. Blakers–Massey comes to mind... $\endgroup$ Feb 9, 2022 at 5:05
  • 1
    $\begingroup$ I've edited the question to make it clearer that I am seeking various examples, rather than the more binary question of whether it is/isn't ever the case. I have also flagged the question to be made Community Wiki; something I should have done earlier. $\endgroup$
    – Wojowu
    Feb 9, 2022 at 16:25

3 Answers 3

19
$\begingroup$

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.

$\endgroup$
5
  • 2
    $\begingroup$ Although this hasn't been discussed yet on Meta, I think immediate self-answers like this should be discouraged (unless perhaps if the answer were to be made a community wiki, which is possible when you click the edit button). There's certainly benefits of having this knowledge here, but it's also possible that every single one of us asks and self-answers everything we know, which would look a bit bizarre. $\endgroup$ Feb 9, 2022 at 3:01
  • $\begingroup$ As it’s currently written, your answer is unclear. Please edit to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers in the help center. $\endgroup$
    – Community Bot
    Feb 9, 2022 at 3:01
  • 3
    $\begingroup$ @NikeDattani In general, SE encourages self-answers for questions which can be considered to be helpful to the community. That said, I completely agree with your concern and agree it should be something to be brought up and considered on Meta. Also, I think for a "big list" kinds of questions I think this is less of a concern - I would still be looking forward to answers coming from other users. $\endgroup$
    – Wojowu
    Feb 9, 2022 at 3:06
  • 1
    $\begingroup$ @Wojowu Yea, I'm not sure how long ago that help center was written, and how many people agree with it. I know SE sites where it's explicitly discouraged, but discussions did take place on Meta. I could ask thousands of questions network-wide and self-answer them! $\endgroup$ Feb 9, 2022 at 3:12
  • $\begingroup$ @NikeDattani I have now posted a question on Meta regarding this issue. $\endgroup$
    – Wojowu
    Feb 9, 2022 at 13:08
6
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thank you for your answer, this is amazing! I would agree that this is without a doubt new mathematics - even if it is inspired by classical results, these "synthetic" versions are certainly of independent interest. It's very intriguing to see that in some areas this phenomenon not only happens, but became a norm! $\endgroup$
    – Wojowu
    Feb 9, 2022 at 19:05
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.