Conjectures associated with A067720

formal-conjectures · oeis · ams-11

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.

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

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://oeis.org/A067720
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/OEIS/67720.lean
Local target: Corpus.OEIS67720.prime_add_one_of_a
Source SHA-256: 7dd689d8f1b5712e9964d62ab46d0914f6b8a6dcbad511c64b2ae1e078a724aa
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record