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