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.

▲

mkl 4 hours ago | parent | next [-]

Kevin Buzzard. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h..., discussed recently here: https://news.ycombinator.com/item?id=49568667

▲

andrewchambers 5 hours ago | parent | prev [-]

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...

	▲	andrewchambers 4 hours ago \| parent \| next [-]
		I was replying to the comment about it being slow to run. I wasn't commenting on understanding it.
	▲	jchanimal 4 hours ago \| parent \| prev [-]
		Then run the annealer and learn from the result.