The takeaway quote from the article is:

> The Lean library isn't just tested and validated, it's proved correct. This allows us to let AIs loose optimizing the code, requiring that they update the proof whenever the implementation materially changes.

To me it's a "that's obvious in hindsight, so why didn't I think of it?" thing.

If you can write a zlib compressor in it, you can write anything in it - so this is a technique that could be applied all problems amenable to formal proofs. Formal proofs are almost never worth the cost when they only prove the absence of bugs. Adding another payback, "you get speed as well", alters that equation.

Definitely merits more than 2 points after 20 hours. It feels like some readers can't look past an LLM being involved.