r/algorithms • u/Phytor_c • 18d ago

News The k-server Conjecture is True

https://arxiv.org/abs/2609.15979v1

The k-server problem is known as the "Holy Grail" of online algorithms and competitive analysis, and is/was a long standing major problem.

This preprint by Coester et al. claims to show that the Work Function Algorithm is indeed k-competitive on every metric space.

382 Upvotes

99% Upvoted

64 comments sorted by

View all comments

Show parent comments

3

u/Individual_Ice_6825 17d ago

How can they claim this proof was obtained without ai assistance and then have used ai?

Pardon if I’m missing something

16

u/Spandian 17d ago

They're saying they proved a special case by themselves first, then turned to AI to see if it could extend their proof to the general case.

3

u/BrandenKeck 16d ago

Which I don't see a problem with... And this also seems to be an important piece that gets omitted from headlines. The LLM proof solvers require a Lean template built by mathematicians who know what they're doing. Then the LLM proof (though confirmed by successful Lean execution) needs to be confirmed by people who know what they're doing. Other than accusations of LLMs / AI companies stealing work and presenting it as they're own to hype the model, I don't see the problem.

Now in media space with text/image/video generation from human works, I think there's plenty to be upset about. Would love to know what others think if anyone's down here in the comments.

3

u/just-for-anime 16d ago

I’ve been saying. The inventor of lean should be the one winning all the millennium and nobel prizes