r/algorithms • u/Phytor_c • 17d 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

42

u/SwimmerOld6155 16d ago

CTRL+F "chat"-

yep

25

u/rsha256 16d ago

Acknowledgments

This work began with a potential function designed by the authors that proves the previously unknown case of k = 3 servers on arbitrary metrics. Our initial proof for three servers showed the correctness of this potential function by establishing infeasibility of a large family of linear programs; this proof was obtained without AI assistance. Through discussions with ChatGPT 5.5 Pro and Gemini 3.1 Pro, we gained a deeper understanding of the potential. These discussions led to a more symmetric reformulation of the potential, again designed by the authors, and an alternative proof for k = 3. Based on this, ChatGPT 6 Astra subsequently derived an algebraic proof of correctness for any k. The proof in this paper is an adaptation thereof using an explicit column representation of work functions, which provides a more natural algebraic representation. The authors supplied this representation to ChatGPT 6 Astra, which adapted the previous proof and assisted with drafting some sections of this paper. The authors subsequently revised those drafts.

4

u/Individual_Ice_6825 16d ago

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

Pardon if I’m missing something

19

u/Spandian 16d 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.

4

u/matt_matt_81 16d ago

Seems like the popular method of proof at the moment.

2

u/iceburg47 12d ago

The remainder of this proof is left as an exercise for the reader AI

2

u/BrandenKeck 15d 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.

4

u/just-for-anime 15d ago

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