It is cool how even for such a "simple looking" problem, we were still unable to prove optimality as of 2020.
Given stuff like arxiv.org/pdf/2107.12475.pdf on Erdős' conjecture on powers of 2, it feels like this one will be somewhere close to computer science/Halting problem issues than number theory. Who knows. This is suggested e.g. at The Busy Beaver Competition: a historical survey by Pascal Michel.