← Back to context Comment by nradov 1 day ago There's an opportunity to build a Lean "optimizer" which automatically simplifies existing proofs. 1 comment nradov Reply stabbles 21 hours ago 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.
stabbles 21 hours ago 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.
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.