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, I wanted to ask, are there any "success stories" in which formalization efforts have lead to new mathematical discoveries?

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?