What is the shortest sequence of decomposition a given single-qubit unitary gate

Question

Given a single-qubit unitary matrix, can we find the shortest sequence of Clifford + T gates that correspond to that unitary?

According to Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates , which is Solovay-Kitaev decomposition, I learned single-qubit decomposition may need $O(\log^{3.97} (1/\delta))$ clifford+T gates with the accuracy $\delta$.

And later many optimization is worked on it. For example: Synthesis of unitaries with Clifford+T circuits

So I want to know if there exists a shortest sequence of Clifford + T gates that correspond to decompose any single-qubit unitary into Clifford+T? If it existed, what is commonly used in current compiler?

Answer 1

In the abstract of the first paper you cite (which, incidentally, is not Solovay-Kitaev, it's an improvement), they say

We report an efficient synthesis algorithm, with an exact optimality guarantee on the number of Hadamard and T gates used

In other words, this is the best that can be done. It yields the shortest possible sequence. This best is $O(\log\frac{1}{\delta})$ Hadamard + T.