4 ms·
It's because anthropic vibemathed it. I forgot the name but some other guy is working on a handwritten version of it and I bet it'll be more than just 1 magnitu
by QwenGlazer9000 16d ago
It's because anthropic vibemathed it. I forgot the name but some other guy is working on a handwritten version of it and I bet it'll be more than just 1 magnitude faster.
- andrewchambers 16d agoThey 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 16d 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 16d agoThen run the annealer and learn from the result.
- andrewchambers 16d agoI was replying to the comment about it being slow to run. I wasn't commenting on understanding it.
- devin 16d agoLet’s start with “what would happen” and run the experiment instead of starting with “they could probably”.
- mkl 16d agoKevin Buzzard. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h..., discussed recently here: https://news.ycombinator.com/item?id=49568667 https://news.ycombinator.com/item?id=49568667
- NeuralCoreAI 12d ago[flagged]