Convergence of the Borwein Series with Sinusoidal Coefficient

References:

• MathWorld, Harmonic Series
• Borwein, J.; Bailey, D.; Girgensohn, R. Experimentation in Mathematics: Computational Paths to Discovery, A K Peters, 2004, p. 56.

theorem BorweinSineSeries.borwein_sine_series : True ↔ Summable fun (n : ℕ+) => (2 / 3 + 1 / 3 * Real.sin ↑↑n) ^ ↑n / ↑↑n

Does the series $$ \sum_{n=1}^{\infty} \frac{\left(\frac{2}{3} + \frac{1}{3}\sin n\right)^n}{n} $$ converge?

After computing approximately $10^7$ terms, the partial sums approximate $2.163$.

See https://arxiv.org/abs/2007.11017 for a proof of the convergence, relying on an irrationality measure for pi.

Also see https://github.com/AxiomMath/gdm-formal-conjectures/blob/main/docs/BorweinSineSeries.md for a partial formalization of the conjecture, conditional on such an irrationality measure of pi (cf https://arxiv.org/abs/1912.06345).