Integer values of $\tan(\arctan 1+\arctan 2+\cdots+\arctan n)$ are rare
Ken Ono
math.NT
Jul 7, 2026 · v1
math.CO
TL;DR
Number-theoretic results bounding integer values of arctangent sums were formalized in Lean/Mathlib and produced autonomously by AxiomProver from natural-language statements.
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.
Problem
Amdeberhan, Medina, and Moll conjectured that x_n = tan(sum_{k=1}^n arctan k) is not an integer for n>=5. Prior work verified this only for a density-0.147 set of n.
Approach
The x_n are analyzed via Gaussian integers, writing Z_n = prod(1+ik) = A_n + iB_n with x_n = B_n/A_n and A_n^2+B_n^2 = omega_n = prod(1+k^2). A divisibility barrier shows any integer value m must satisfy K_n | (1+m^2), forcing |m| >= sqrt(K_n - 1). An analytic argument bounds the exceptional set where |x_n| is large. The results were formalized in Lean/Mathlib and generated autonomously by AxiomProver from natural-language statements.
Results
Any integer value satisfies |m| >= e^{(1/2+o(1)) n log n}, and #{1<=n<=N : x_n in Z} = O(log N), so the conjecture holds for a density-one set of n.
| n | K_n | min\ | m\ | | x_n |
|---|
| 1 | 2 | 1 | 1 |
| 2 | 10 | 3 | -3 |
| 3 | 1 | 0 | 0 |
| 4 | 17 | 4 | 4 |
| 5 | 442 | 21 | -9/19 |
K_n, least |m| with K_n | (1+m^2), and x_n for small n
