Conjectures associated with A067720

A067720 lists numbers $k$ such that $\varphi(k^2 + 1) = k \cdot \varphi(k + 1)$, where $\varphi$ is Euler's totient function.

The sequence exhibits a strong connection to primes: for almost all terms $k$, $k + 1$ is prime. The conjecture states that $k = 8$ is the only exception.

References: A067720

def OeisA67720.a (k : ℕ) : Prop

A number $k$ is in the sequence A067720 if $\varphi(k^2 + 1) = k \cdot \varphi(k + 1)$.

Equations

• OeisA67720.a k = ((k ^ 2 + 1).totient = k * (k + 1).totient)

theorem OeisA67720.a_1 : a 1

$1$ is in the sequence A067720.

theorem OeisA67720.a_2 : a 2

$2$ is in the sequence A067720.

theorem OeisA67720.a_4 : a 4

$4$ is in the sequence A067720.

theorem OeisA67720.a_6 : a 6

$6$ is in the sequence A067720.

theorem OeisA67720.a_8 : a 8

$8$ is in the sequence A067720.

theorem OeisA67720.a_10 : a 10

$10$ is in the sequence A067720.

theorem OeisA67720.a_of_primes {k : ℕ} (hk : Nat.Prime (k + 1)) (hk' : Nat.Prime (k ^ 2 + 1)) : a k

If $k + 1$ and $k^2 + 1$ are both prime, then $k$ is in the sequence.

theorem OeisA67720.prime_add_one_of_a {k : ℕ} (h : a k) (hne : k ≠ 8) : Nat.Prime (k + 1)

For members of the sequence other than $8$, we have $k + 1$ is prime.