Beautiful examples of "XAndCommutedX helps math coders"

Stream: general

[Juho Kupiainen]

The aim of Lean is for math to help programmers and for programmers to help math. What are the most beautiful realizations of this?

[Kevin Buzzard]

I think that Gouezel's discovery of an error in the published math literature was quite an interesting realization (using Isabelle/HOL not Lean though).