| ▲ | andrewchambers 5 hours 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 . | ||||||||||||||
| ▲ | devin 3 hours ago | parent | next [-] | |||||||||||||
Let’s start with “what would happen” and run the experiment instead of starting with “they could probably”. | ||||||||||||||
| ▲ | maths_math 4 hours ago | parent | prev [-] | |||||||||||||
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... | ||||||||||||||
| ||||||||||||||