Yeah, code golfing for lean would be amazing, especially if they can make the proof to Fourier's Last Theorem fit in the margin.

Extra credits if it is proven that the proof cannot be reduced any further.