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.