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

For $n\ge 1$, we let $$x_n:=\tan (\sum _{k=1}^n\arctan k)\mathrm{.}$$ In 2008, Amdeberhan, Medina, and Moll conjectured that $x_n\in ̸\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 $\mathrm{\mid }m\mathrm{\mid }\ge e^{(1\mathrm{/}2+o(1))n\log n}$, which we use to deduce that $$\mathrm{\#}\{1\le n\le N:x_n\in \mathbb{Z}\}=O(\log N)\mathrm{.}$$ 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.