[drainyard]

Something like CRLS? That is fairly implementable pseudocode, but maybe still too hand wavey at times.

[abc_lisper]

It really is; it's irritating that they say it can be trivially proved with induction, robbing me from understanding the crux of the problem.