Integer values of $\tan (\arctan 1+\arctan 2+\cdots +\arctan n)$ are rare

Abstract

For $n\ge 1$, we let $$x_n:=\tan \left(\sum _{k=1}^n\arctan k\right).$$ In 2008, Amdeberhan, Medina, and Moll conjectured that $x_n\notin \mathbb{Z}$ for every $n\ge 5$. This was known for a set of positive integers of density $\frac{120}{817}\approx 0.1469$. We prove that an integer value $x_n=m$ satisfies $|m|\ge e^{(1/2+o(1))n\log n}$, which we use to deduce that $$\#\{1\le n\le N:x_n\in \mathbb{Z}\}=O(\log N).$$ In particular, the conjecture holds for a density-one set of $n$. The results in this note were formalized in Lean/Mathlib and produced autonomously by AxiomProver from natural-language statements.

9 pages. Proof uses only classical estimates (Stirling, Mertens, Chebyshev). Lean/Mathlib formalization at github.com/AxiomMath/TanArctan