There's an opportunity to build a Lean "optimizer" which automatically simplifie... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

nradov 18 days ago | parent | context | favorite | on: On the Navier–Stokes Millennium Prize Problem

There's an opportunity to build a Lean "optimizer" which automatically simplifies existing proofs.

stabbles 18 days 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.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact