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

Abstract

For $n\ge1$, we let $$x_n:=\tan\bigl(\sum_{k=1}^{n}\arctan k\bigr).$$ In 2008, Amdeberhan, Medina, and Moll conjectured that $x_n\not \in \mathbb{Z}$ for every $n\ge5$. This was known for a set of positive integers of density $\tfrac{120}{817}\approx0.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\leq 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.

Disclosure

“INTEGER VALUES OF tan(arctan 1 + arctan 2 + · · · + arctan n) ARE RARE 9 Declaration of generative AI and AI-assisted technologies in the manuscript preparation process As described in the preceding appendix, AxiomProver was used to produce and formally verify, in Lean, the proofs of the results of this paper. The exposition w”

PDF page 9

Classification

Code generation, completion, or debugging

Multiplier

2

Verified

2026-08-24T00:34:09.244Z

Structural counts