TanArctanSum.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

19 declarations, 6 contain sorry, 0 declared as axioms

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.

Imports (1)

FormalConjecturesUtil

def Arxiv.«2607.05739».gaussProd $Z_n = \prod_{k=1}^n (1 + ik)$, in the Gaussian integers line 40 source
Source documentation
$Z_n = \prod_{k=1}^n (1 + ik)$, in the Gaussian integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GaussianInt
Proof uses: Finset.prod, Neg.neg, Int, OfNat.ofNat, Finset.Icc, Zsqrtd.mk
8 instances, coercions and auxiliary constants left out.
```
def gaussProd (n : ℕ) : GaussianInt := ∏ k ∈ Finset.Icc 1 n, (⟨1, (k : ℤ)⟩ : GaussianInt)
```
def Arxiv.«2607.05739».A $A_n = \operatorname{Re} Z_n$ line 43 source
Source documentation
$A_n = \operatorname{Re} Z_n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: Zsqrtd.re, Neg.neg, OfNat.ofNat, Arxiv.«2607.05739».gaussProd
2 instances, coercions and auxiliary constants left out.
```
def A (n : ℕ) : ℤ := (gaussProd n).re
```
Mentions: Arxiv.«2607.05739».gaussProd
def Arxiv.«2607.05739».B $B_n = \operatorname{Im} Z_n$ line 46 source
Source documentation
$B_n = \operatorname{Im} Z_n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: Zsqrtd.im, Neg.neg, OfNat.ofNat, Arxiv.«2607.05739».gaussProd
2 instances, coercions and auxiliary constants left out.
```
def B (n : ℕ) : ℤ := (gaussProd n).im
```
Mentions: Arxiv.«2607.05739».gaussProd
def Arxiv.«2607.05739».x $x_n = \tan\left(\sum_{k=1}^n \arctan k\right) = B_n / A_n$ line 49 source
Source documentation
$x_n = \tan\left(\sum_{k=1}^n \arctan k\right) = B_n / A_n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: HDiv.hDiv, Arxiv.«2607.05739».B, Arxiv.«2607.05739».A
4 instances, coercions and auxiliary constants left out.
```
noncomputable def x (n : ℕ) : ℚ := (B n : ℚ) / (A n : ℚ)
```
Mentions: Arxiv.«2607.05739».B, Arxiv.«2607.05739».A
def Arxiv.«2607.05739».IsIntegerValue $x_n$ takes an integer value line 57 source
Source documentation
$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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Dvd.dvd, Int, Arxiv.«2607.05739».A, Arxiv.«2607.05739».B
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def IsIntegerValue (n : ℕ) : Prop := A n ∣ B n
```
Mentions: Arxiv.«2607.05739».A, Arxiv.«2607.05739».B
instance Arxiv.«2607.05739».(instance at line 59) line 59 source
theorem Arxiv.«2607.05739».tan_arctan_sum_not_integer Conjecture (Amdeberhan-Medina-Moll, 2008) sorry line 67 source
Source documentation
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.

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Not, Arxiv.«2607.05739».IsIntegerValue
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem tan_arctan_sum_not_integer :
    answer(sorry) ↔ ∀ n : ℕ, 5 ≤ n → ¬ IsIntegerValue n := by
…
```
Mentions: Arxiv.«2607.05739».IsIntegerValue
theorem Arxiv.«2607.05739».x_succ $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 sorry line 74 source
Source documentation
$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.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Rat, Arxiv.«2607.05739».x, HAdd.hAdd, HDiv.hDiv, HSub.hSub, HMul.hMul
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem x_succ (n : ℕ) (hn : 1 ≤ n) :
    x (n + 1) = (x n + (n + 1)) / (1 - (n + 1) * x n) := by
…
```
Mentions: Arxiv.«2607.05739».x
theorem Arxiv.«2607.05739».x_eq_tan_sum_arctan $x_n$ is the tangent of the partial sum of arctangents it is named for sorry line 80 source
Source documentation
$x_n$ is the tangent of the partial sum of arctangents it is named for.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Real, Arxiv.«2607.05739».x, Real.tan, Finset.sum, Finset.Icc, Real.arctan
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem x_eq_tan_sum_arctan (n : ℕ) (hn : 1 ≤ n) :
    (x n : ℝ) = Real.tan (∑ k ∈ Finset.Icc 1 n, Real.arctan k) := by
…
```
Mentions: Arxiv.«2607.05739».x
def Arxiv.«2607.05739».omega $\omega_n = A_n^2 + B_n^2 = \prod_{k=1}^n (1 + k^2)$, the norm of $Z_n$ line 85 source
Source documentation
$\omega_n = A_n^2 + B_n^2 = \prod_{k=1}^n (1 + k^2)$, the norm of $Z_n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, HPow.hPow, Int.natAbs, Arxiv.«2607.05739».A, OfNat.ofNat, Arxiv.«2607.05739».B
7 instances, coercions and auxiliary constants left out.
```
def omega (n : ℕ) : ℕ := (A n).natAbs ^ 2 + (B n).natAbs ^ 2
```
Mentions: Arxiv.«2607.05739».A, Arxiv.«2607.05739».B
def Arxiv.«2607.05739».kernel 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 line 89 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.prod, Finset.filter, Odd, Finsupp, Nat.factorization, Arxiv.«2607.05739».omega, Nat.primeFactors
7 instances, coercions and auxiliary constants left out.
```
def kernel (n : ℕ) : ℕ :=
…
```
def Arxiv.«2607.05739».angleSum $a_n = \sum_{k=1}^n \arctan(1/k)$ line 93 source
Source documentation
$a_n = \sum_{k=1}^n \arctan(1/k)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.sum, Finset.Icc, OfNat.ofNat, Real.arctan, HDiv.hDiv
11 instances, coercions and auxiliary constants left out.
```
noncomputable def angleSum (n : ℕ) : ℝ := ∑ k ∈ Finset.Icc 1 n, Real.arctan (1 / (k : ℝ))
```
def Arxiv.«2607.05739».exceptional The exceptional set $E = \{n \geq 5 : |x_n| > n/2 + 1\}$ line 97 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, And, LE.le, OfNat.ofNat, Or, Eq, Int, Arxiv.«2607.05739».A, LT.lt, Rat, HAdd.hAdd, HDiv.hDiv, abs, Arxiv.«2607.05739».x
13 instances, coercions and auxiliary constants left out.
```
def exceptional : Set ℕ := {n | 5 ≤ n ∧ (A n = 0 ∨ ((n : ℚ) / 2 + 1 < |x n|))}
…
```
Mentions: Arxiv.«2607.05739».A, Arxiv.«2607.05739».x
theorem Arxiv.«2607.05739».kernel_dvd_of_eq_intCast sorry line 105 source
depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Ne, Int, Arxiv.«2607.05739».A, Eq, Rat, Arxiv.«2607.05739».x, And, Dvd.dvd, Arxiv.«2607.05739».kernel, HAdd.hAdd, HPow.hPow, LT.lt, Real, Real.sqrt, HSub.hSub, abs
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«2607.05739».exists_near_half_pi sorry line 114 source
depends on sorry what this means
Statement uses: Nat, Membership.mem, Set, Arxiv.«2607.05739».exceptional, Exists, Int, LT.lt, Real, abs, HSub.hSub, Arxiv.«2607.05739».angleSum, HMul.hMul, HDiv.hDiv, Real.pi, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«2607.05739».exceptional_ncard_le sorry line 122 source
depends on sorry what this means
Statement uses: Exists, Real, Nat, And, LT.lt, OfNat.ofNat, LE.le, Set.ncard, Inter.inter, Set, Arxiv.«2607.05739».exceptional, Set.Icc, HMul.hMul, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Arxiv.«2607.05739».isIntegerValue_of_le_four The four integer values the conjecture leaves out line 128 source
Source documentation
The four integer values the conjecture leaves out.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Arxiv.«2607.05739».IsIntegerValue, OfNat.ofNat, Nat
Proof uses: And.intro, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem isIntegerValue_of_le_four :
    IsIntegerValue 1 ∧ IsIntegerValue 2 ∧ IsIntegerValue 3 ∧ IsIntegerValue 4 := by
…
```
Mentions: Arxiv.«2607.05739».IsIntegerValue
theorem Arxiv.«2607.05739».x_values $x_1 = 1$, $x_2 = -3$, $x_3 = 0$, $x_4 = 4$ line 134 source
Source documentation
$x_1 = 1$, $x_2 = -3$, $x_3 = 0$, $x_4 = 4$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Eq, Rat, Arxiv.«2607.05739».x, OfNat.ofNat, Nat, Neg.neg
Proof uses: And.intro, Eq.mpr, HDiv.hDiv, Arxiv.«2607.05739».B, Arxiv.«2607.05739».A, id, congrArg, Arxiv.«2607.05739».x.eq_1, Zsqrtd.re, Int, Arxiv.«2607.05739».gaussProd, Arxiv.«2607.05739».A.eq_1, Zsqrtd.im, Arxiv.«2607.05739».B.eq_1, of_eq_true, Eq.trans, True, congrFun', congr, Zsqrtd.mk and 62 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem x_values : x 1 = 1 ∧ x 2 = -3 ∧ x 3 = 0 ∧ x 4 = 4 := by
…
```
Mentions: Arxiv.«2607.05739».x
theorem Arxiv.«2607.05739».not_isIntegerValue_of_mem_Icc_five_ten The conjecture holds at the first few values it covers line 139 source
Source documentation
The conjecture holds at the first few values it covers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Not, Arxiv.«2607.05739».IsIntegerValue
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem not_isIntegerValue_of_mem_Icc_five_ten :
    ∀ n ∈ Finset.Icc 5 10, ¬ IsIntegerValue n := by
…
```
Mentions: Arxiv.«2607.05739».IsIntegerValue