Only a bit more than two months ago, a new formula for Kazhdan-Lusztig
polynomials was found by Google's deep learning subsidiary: DeepMind (the same machine-learning company that wrote AlphaGo to beat humans at the board game Go). This formula is presented as Theorem 3.7 in the above-linked paper, and the authors conjectured in the same paper that the formula gives the right answer for any hypercube decomposition (which they indeed checked computationally for all of the Bruhat intervals up to $S_9$, which turned out to be more than a million of them). This conjecture which they computationally found to be very likely true, implies the combinatorial invariance conjecture for symmetric groups, which has been unproven since it was first formulated the 1980s.
The proof of Theorem 3.7 is given in Sections 4-5 of the above-linked-paper, but and is very much a "pen-and-paper" proof, but the theorem itself was discovered amidst the training of machine learning models to predict Kazhdan-Lusztig polynomials from Bruhat graphs, in Nature (2021) "Advancing mathematics by guiding human intuition with AI" which was only published about 2 months ago (Fig 3 shows which hypercube edges are the most important ones as determined from a saliency analysis, and these turned out to be precisely the edges related to the new theorem). Carlo Beenakker called this "the first significant advance in pure mathematics generated by artificial intelligence" in the highest-voted answer to "Breakthroughs in Mathematics in 2021" on MathOverflow (an answer on which you were the first to write a comment!).
Overall, the combinatorial invariance conjecture for symmetric
groups remains unproven, but machine-learning helped to discover a "Lemma" which is very likely to be a part of the proof. I would call this a major "success of machine learning in theorem proving", but about this part of your question:
"Are there other applications of machine-learning to constructing proofs in any proof assistant that attained a success of at least this magnitude - i.e. finding somewhat better versions of existing proofs, if not entirely new proofs?"
I hope I'm wrong, but even for proofs done by theorem provers without machine learning, the ones I know were not for entirely new proofs but for finding somewhat better versions of existing proofs. In the case I described above, a new proof would rely on a Lemma which the saliency analysis (a machine learning technique borrowed from the computer vision community) was able to help find.