Convergent subsequence for sin(n)

Define a sequence $(a_n)_{n = 1}^{\infty}$ of real numbers by $a_n = \sin(n)$. This sequence is bounded (by $\pm1$), and so by the Bolzano-Weierstrass Theorem, there exists a convergent subsequence.

My question is this: Is there any way to construct an explicit convergent subsequence?

Naïvely, I tried considering the subsequence $$\sin(3), \,\sin(31), \,\sin(314), \,\sin(3141),\, \sin(31415),\, \dots$$ hoping it would converge to $0$, but I was unable to prove this (and I think it's probably not even true).

Solution 1:

This isn't a very analytic way of doing it but consider the continued fraction expansion $\pi = [a_0; a_1, a_2, \ldots]$. Generally we know that, if $p_n/q_n$ are the convergents to $\pi$ then $|q_n\pi - p_n| \leq 1/q$ so the $p_n$ are the closest integers to being multiples of $\pi$ so (with slight abuse of notation) $\sin(p_n) \rightarrow \sin m\pi = 0$ with $n \rightarrow \infty$ meaning that this is an explicit construction of the sort that you're after.