3 ms·
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 .
by andrewchambers 21d ago
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 .
- maths_math 21d agoWhat 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...
- jchanimal 21d agoThen run the annealer and learn from the result.
- andrewchambers 21d agoI was replying to the comment about it being slow to run. I wasn't commenting on understanding it.
- devin 21d agoLet’s start with “what would happen” and run the experiment instead of starting with “they could probably”.