First off, the question itself is disparate. You need some version of the Solovay-Kitaev theorem for optimizing a sub-circuit that acts on a single qubit, and you can also use it for two or three qubits. Moreover, the original Solovay-Kitaev theorem is for completely general gate sets, while there are now nearly optimal single-qubit algorithms for special gate sets, in particular Ross-Selinger for the popular Clifford+T gate set.
Circuit optimization for many qubits is a very different scene, except in that you need to know how to play one key on a piano on the way to playing all 88 of them. For comparison, circuit optimization for a few classical bits is trivial, but it looks intractable even for log(n) input bits, never mind for n input bits (where even checking whether two circuits do the same thing is NP-hard). Quantum circuit optimization for many qubits suffers from the same diseases and possibly worse diseases. In both the classical and quantum cases, general circuit optimization invites ad hoc algorithms that you can always try for any purpose, for example machine learning with neural nets.
There is also a big difference between making tools vs using them. They are both worthwhile programming projects, because the tools have to come from somewhere. To make a new tool, you don't necessarily need a comprehensive QC platform such as Qiskit; you can often get pretty far with Python or (say) Sage.
To expand on that last point, I would certainly applaud a programming project to implement and refine my new Solovay-Kitaev-type algorithm. It probably wouldn't be hot-off-the-press quantum engineering, but it could be good as quantum computer science for its own sake. It's true that my paper hasn't yet been published in a journal, but (a) that isn't always real verification either, and (b) I have explained it to various people. Whenever someone implements an algorithm, then I think that that counts as a step towards verifying that it works.
