1. FormalConjectures
  2. Arxiv
  3. «2607.05739»
  4. TanArctanSum
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

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

References:

    arxiv/2607.05739 Integer values of $\tan(\arctan 1+\arctan 2+\cdots+\arctan n)$ are rare by Ken Ono

    [AMM08] T. Amdeberhan, L. A. Medina, and V. H. Moll, Arithmetical properties of a sequence arising from an arctangent sum, J. Number Theory 128 (2008), no. 6, 1807-1846.

    TanArctan, a Lean formalisation of the three results of [Ono26], MIT licensed. Its P, A, B and x are the definitions used here.

open Finsetnamespace Arxiv.«2607.05739»

$Z_n = \prod_{k=1}^n (1 + ik)$, in the Gaussian integers.

def gaussProd (n : ℕ) : GaussianInt := ∏ k ∈ Finset.Icc 1 n, (⟨1, (k : ℤ)⟩ : GaussianInt)

$A_n = \operatorname{Re} Z_n$.

def A (n : ℕ) : ℤ := (gaussProd n).re

$B_n = \operatorname{Im} Z_n$.

def B (n : ℕ) : ℤ := (gaussProd n).im

$x_n = \tan\left(\sum_{k=1}^n \arctan k\right) = B_n / A_n$.

noncomputable def x (n : ℕ) : ℚ := (B n : ℚ) / (A n : ℚ)

$x_n$ takes an integer value.

Stated as $A_n \mid B_n$ rather than as ∃ m : ℤ, x n = m, so that it still says the right thing if $A_n$ were ever $0$. There $x_n$ is a pole of the tangent rather than an integer, but (B n : ℚ) / 0 is 0 in Lean and would count as one. The two agree whenever $A_n \neq 0$, which holds for every $n \leq 3000$.

def IsIntegerValue (n : ℕ) : Prop := A n ∣ B ninstance (n : ℕ) : Decidable (IsIntegerValue n) := n:ℕ⊢ Decidable (IsIntegerValue n) n:ℕ⊢ Decidable (A n ∣ B n); All goals completed! 🐙

Conjecture (Amdeberhan-Medina-Moll, 2008). For every integer $n \geq 5$, the value $$x_n = \tan(\arctan 1 + \arctan 2 + \cdots + \arctan n)$$ is not an integer.

@[category research open, AMS 11] theorem tan_arctan_sum_not_integer : answer(sorry) ↔ ∀ n : ℕ, 5 ≤ n → ¬ IsIntegerValue n := ⊢ True ↔ ∀ (n : ℕ), 5 ≤ n → ¬IsIntegerValue n All goals completed! 🐙

$x_n$ satisfies $x_1 = 1$ and $x_n = \dfrac{x_{n-1} + n}{1 - n x_{n-1}}$, which is the tangent addition formula.

@[category textbook, AMS 11] theorem x_succ (n : ℕ) (hn : 1 ≤ n) : x (n + 1) = (x n + (n + 1)) / (1 - (n + 1) * x n) := n:ℕhn:1 ≤ n⊢ x (n + 1) = (x n + (↑n + 1)) / (1 - (↑n + 1) * x n) All goals completed! 🐙

$x_n$ is the tangent of the partial sum of arctangents it is named for.

@[category textbook, AMS 11] theorem x_eq_tan_sum_arctan (n : ℕ) (hn : 1 ≤ n) : (x n : ℝ) = Real.tan (∑ k ∈ Finset.Icc 1 n, Real.arctan k) := n:ℕhn:1 ≤ n⊢ ↑(x n) = Real.tan (∑ k ∈ Icc 1 n, Real.arctan ↑k) All goals completed! 🐙

$\omega_n = A_n^2 + B_n^2 = \prod_{k=1}^n (1 + k^2)$, the norm of $Z_n$.

def omega (n : ℕ) : ℕ := (A n).natAbs ^ 2 + (B n).natAbs ^ 2

The squarefree kernel $K_n$ of $\omega_n$: the product of the primes dividing it to an odd power, so 1 when there are none.

def kernel (n : ℕ) : ℕ := ∏ p ∈ (omega n).primeFactors.filter (fun p => Odd ((omega n).factorization p)), p

$a_n = \sum_{k=1}^n \arctan(1/k)$.

noncomputable def angleSum (n : ℕ) : ℝ := ∑ k ∈ Finset.Icc 1 n, Real.arctan (1 / (k : ℝ))

The exceptional set $E = {n \geq 5 : |x_n| > n/2 + 1}$. An index with $A_n = 0$ is a pole of the tangent rather than a large value, and is counted in, reading $|x_n|$ as infinite.

def exceptional : Set ℕ := {n | 5 ≤ n ∧ (A n = 0 ∨ ((n : ℚ) / 2 + 1 < |x n|))}

An integer value is divisible in a way that forces it to be large: if $x_n = m$ then $K_n \mid 1 + m^2$, and $|m| \geq \sqrt{K_n - 1}$ once $K_n > 1$.

@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/AxiomMath/TanArctan/blob/5382d3c20ee3f30e2cbd84362eb07a7e93250348/output/solution.lean#L176"] theorem kernel_dvd_of_eq_intCast {n : ℕ} (hn : 1 ≤ n) (hA : A n ≠ 0) {m : ℤ} (hx : x n = (m : ℚ)) : ((kernel n : ℤ) ∣ (1 + m ^ 2)) ∧ (1 < kernel n → Real.sqrt ((kernel n : ℝ) - 1) ≤ |(m : ℝ)|) := n:ℕhn:1 ≤ nhA:A n ≠ 0m:ℤhx:x n = ↑m⊢ ↑(kernel n) ∣ 1 + m ^ 2 ∧ (1 < kernel n → √(↑(kernel n) - 1) ≤ |↑m|) All goals completed! 🐙

Every exceptional index sits close to a multiple of $\pi/2$ in angle.

@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/AxiomMath/TanArctan/blob/5382d3c20ee3f30e2cbd84362eb07a7e93250348/output/solution.lean#L453"] theorem exists_near_half_pi {n : ℕ} (hn : n ∈ exceptional) : ∃ j : ℤ, |angleSum n - (j : ℝ) * (Real.pi / 2)| < 2 / (n : ℝ) := n:ℕhn:n ∈ exceptional⊢ ∃ j, |angleSum n - ↑j * (Real.pi / 2)| < 2 / ↑n All goals completed! 🐙

The exceptional indices are sparse: $#(E \cap [1,N]) = O(\log N)$. This is the sense in which integer values are rare, and it is what [Ono26] proves.

@[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/AxiomMath/TanArctan/blob/5382d3c20ee3f30e2cbd84362eb07a7e93250348/output/solution.lean#L975"] theorem exceptional_ncard_le : ∃ (C : ℝ) (N₀ : ℕ), 0 < C ∧ ∀ N : ℕ, N₀ ≤ N → ((exceptional ∩ Set.Icc 1 N).ncard : ℝ) ≤ C * Real.log N := ⊢ ∃ C N₀, 0 < C ∧ ∀ (N : ℕ), N₀ ≤ N → ↑(exceptional ∩ Set.Icc 1 N).ncard ≤ C * Real.log ↑N All goals completed! 🐙

The four integer values the conjecture leaves out.

@[category test, AMS 11] theorem isIntegerValue_of_le_four : IsIntegerValue 1 ∧ IsIntegerValue 2 ∧ IsIntegerValue 3 ∧ IsIntegerValue 4 := ⊢ IsIntegerValue 1 ∧ IsIntegerValue 2 ∧ IsIntegerValue 3 ∧ IsIntegerValue 4 ⊢ IsIntegerValue 1⊢ IsIntegerValue 2⊢ IsIntegerValue 3⊢ IsIntegerValue 4 ⊢ IsIntegerValue 1⊢ IsIntegerValue 2⊢ IsIntegerValue 3⊢ IsIntegerValue 4 All goals completed! 🐙

$x_1 = 1$, $x_2 = -3$, $x_3 = 0$, $x_4 = 4$.

⊢ ↑(gaussProd 4).im / ↑(gaussProd 4).re = 4; All goals completed! 🐙

The conjecture holds at the first few values it covers.

@[category test, AMS 11] theorem not_isIntegerValue_of_mem_Icc_five_ten : ∀ n ∈ Finset.Icc 5 10, ¬ IsIntegerValue n := ⊢ ∀ n ∈ Icc 5 10, ¬IsIntegerValue n All goals completed! 🐙end Arxiv.«2607.05739»