This problem is very much open. Cheng Yong calls *Harrington's $\star$* the assumption that there is a real $x$ such that all $x$-admissible ordinals are $L$-cardinals. From the work of Yong we know that Second (or even Third) order arithmetic does not suffice to prove that Harrington's $\star$ implies the existence of $0^\sharp$. Whether this was possible was originally asked by Woodin, who proved that Second order arithmetic suffices to show that $\mathrm{Det}(\Sigma^1_1)$ implies Harrington's $\star$. This appears in Yong's dissertation, *Analysis of Martin-Harrington theorem* "$\mathrm{Det}(\Sigma^1_1)\leftrightarrow 0^\sharp$ exists" *in higher order arithmetic*, National University of Singapore, 2012. Here, - Second order arithmetic, $Z_2$, is formalized as: $(\mathsf{ZFC}-$ Power set axiom$)+$ All sets are countable. - Third order arithmetic is $(\mathsf{ZFC}-$ Power set axiom$)+\mathcal P(\omega)$ exists $+$ All sets have size at most continuum. - Fourth order arithmetic, which Yong shows proves that Harrington's $\star$ implies the existence of $0^\sharp$, is $(\mathsf{ZFC}-$ Power set axiom$)+\mathcal P^2(\omega)$ exists $+$ All sets have size at most $2^{2^{\aleph_0}}$. Ralf Schindler has further clarified the situation: $Z_2+$ Harrington's $\star$ is *equiconsistent* with $\mathsf{ZFC}+$ There is a [remarkable][1] cardinal. As question 8.0.14 in his thesis, Yong asks whether $Z_2$ proves Harrington theorem. This is tricky, since $Z_2$ proves that $\mathrm{Det}(\mathbf\Sigma^1_1)$ is equiconsistent with "For all reals $x$, $x^\sharp$ exists." The reason why the lightface version is open, Yong admits, is that the only route we have from $\mathrm{Det}(\Sigma^1_1)$ to the existence of $0^\sharp$ is via Harrington's $\star$, so the question is effectively asking for a different argument. There are several sufficiently different proofs of Harrington's theorem. For example, there is the argument in **Recursive Aspects of Descriptive Set Theory** by Mansfield and Weitkamp, via non-$\omega$-models of $\mathsf{KP}$. There is Harrington's original proof, using Steel's forcing. There is Sami's proof, from *Analytic determinacy and $0^\sharp$: A forcing-free proof of Harrington's theorem*. All use Harrington's $\star$ in an essential fashion. The question of whether a different route is possible has been studied, of course, but unsuccessfully. [1]: http://cantorsattic.info/Remarkable