logoalt Hacker News

andrewchambers • yesterday at 10:02 PM • 2 replies • view on HN

They could probably vibe-optimize it if they cared.

What would happen if they give an equivalent agent swarm the proof and a target to reduce runtime .

Replies

devin • yesterday at 11:36 PM

Let’s start with “what would happen” and run the experiment instead of starting with “they could probably”.

maths_math • yesterday at 10:24 PM

What would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...

➕ show 2 replies