Integrality of the arctangent-sum sequence

For xₙ=tan(Σₖ₌₁ⁿ arctan k), is xₙ nonintegral for every n≥5? Amdeberhan, Medina and Moll posed the all-index conjecture; a density-one result leaves possible exceptional indices.

Why it matters and what counts as progress

Why it matters: The all-index conjecture is stronger than proving nonintegrality for almost all indices; bounds on exceptions measure the gap.

What counts as progress: Exclude integer values for a larger set of indices, sharpen bounds on exceptions, or settle the every-index conjecture.

How the problem developed

2008 · Conjecture [1]
Theodore Amdeberhan, Luis Medina and Victor Moll Conjectured that xₙ = tan(Σₖ₌₁ⁿ arctan k) is never an integer for n≥5; earlier results ruled out integer values on a subset of density 120/817.
7 Jul 2026 · Partial result [1]
Ken Ono and AxiomProver Proved that integer values are exceptionally large and occur for only O(log N) indices through N, establishing nonintegrality for a density-one set of indices; the paper reports an autonomous Lean formalization.

AI contribution

Integer values of tan(arctan 1 + arctan 2 + ⋯ + arctan n) are rare

Ken Ono

AxiomProver proved in Lean that an integral x_n forces the squarefree kernel K_n to divide 1+m² with |m|≥√(K_n−1), that large exceptional x_n lie near a π/2 lattice point, and that the exceptional set has O(log N) members through N. Ono combines these with his asymptotic lower bound for K_n to show nonintegrality for almost all n.

AI involvementAI-led

ImportanceNotable

Technical verificationFormal (Lean 4.28.0 / Mathlib)

Human understandingFull