Here <https://cacm.acm.org/magazines/2017/8/219606-the-science-of-...> is an article about a computer-generated proof of a combinatorial problem in number theory. Although you could characterise the proof as "just long", I think that the article may offer a different perspective on why proofs of this nature are interesting and useful.