Consider the next problem. Given a large oriented graph find its diameter: maximal length over all shortest directed paths between every pair of vertices. Graph is strongly connected. It is allowed to give lower and upper bounds on the answer. Time complexity should be linear or close to it.
Suppose I solved the problem and I want to prove it. Moreover I want the proof can be checked in linear time: graph is large.
Lower bound is easy. Just let me give two vertices on neccessary distance. Upper bound is harder. I can give a vertex and ask to estimate the furthest vertex reachable by forward, and then by backward, edges. Then I sum up these distances and call it upper bound.
The problem that my upper bound doesn't look tight. Can anybody suggest something better?