FormalConjectures.OEIS.«67720»

/-
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

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.

Reference: A67720


namespace OeisA67720


open Nat

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

def A (k : ℕ) : Prop :=
  φ (k ^ 2 + 1) = k * φ (k + 1)

$1$ is in the sequence A067720.

@[category test, AMS 11]
theorem a_1 : A 1 := by⊢ A 1 norm_num [A]All goals completed! 🐙

$2$ is in the sequence A067720.

@[category test, AMS 11]
theorem a_2 : A 2 := by⊢ A 2
  simp +decide only [A]All goals completed! 🐙

$4$ is in the sequence A067720.

@[category test, AMS 11]
theorem a_4 : A 4 := by⊢ A 4
  simp +decide only [A]All goals completed! 🐙

$6$ is in the sequence A067720.

@[category test, AMS 11]
theorem a_6 : A 6 := by⊢ A 6
  simp +decide only [A]All goals completed! 🐙

$8$ is in the sequence A067720.

@[category test, AMS 11]
theorem a_8 : A 8 := by⊢ A 8
  simp +decide only [A]All goals completed! 🐙

$10$ is in the sequence A067720.

@[category test, AMS 11]
theorem a_10 : A 10 := by⊢ A 10
  simp +decide only [A]All goals completed! 🐙

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

@[category textbook, AMS 11]
theorem a_of_primes {k : ℕ} (hk : (k + 1).Prime) (hk' : (k ^ 2 + 1).Prime) : A k := byk:ℕhk:Nat.Prime (k + 1)hk':Nat.Prime (k ^ 2 + 1)⊢ A k
  rw [A, totient_prime hk', totient_prime hk, Nat.add_sub_cancel, Nat.add_sub_cancel, sq]All goals completed! 🐙

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

@[category research open, AMS 11]
theorem declaration uses 'sorry'prime_add_one_of_a {k : ℕ} (h : A k) (hne : k ≠ 8) : (k + 1).Prime := byk:ℕh:A khne:k ≠ 8⊢ Nat.Prime (k + 1)
  sorryAll goals completed! 🐙


end OeisA67720