3 ms·
There's an opportunity to build a Lean "optimizer" which automatically simplifies existing proofs.
by nradov 1mo ago
There's an opportunity to build a Lean "optimizer" which automatically simplifies existing proofs.
- stabbles 1mo agoYeah, 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.