/-
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 FormalConjecturesUtilDivisibility of $2^n + 1$ by $n$
A56777 lists composite numbers $n$ satisfying both $\varphi(n+12) = \varphi(n) + 12$ and $\sigma(n+12) = \sigma(n) + 12$.
The conjectures state identities connecting A56777 and prime quadruples (A7530), as well as congruences satisfied by the members of A56777.
References:
namespace OeisA56777open Natopen scoped ArithmeticFunction.sigmaA composite number $n$ is in the sequence A56777 if it satisfies both $\varphi(n+12) = \varphi(n) + 12$ and $\sigma(n+12) = \sigma(n) + 12$.
def A (n : ℕ) : Prop :=
¬n.Prime ∧ 1 < n ∧ totient (n + 12) = totient n + 12 ∧ σ 1 (n + 12) = σ 1 n + 12A number $n$ comes from a prime quadruple $(p, p+2, p+6, p+8)$ if $n = p(p+8)$ for some prime $p$ where $p$, $p+2$, $p+6$, $p+8$ are all prime.
def ComesFromPrimeQuadruple (n : ℕ) : Prop :=
∃ p : ℕ, p.Prime ∧ (p + 2).Prime ∧ (p + 6).Prime ∧ (p + 8).Prime ∧ n = p * (p + 8)$65$ is in the sequence A56777.
@[category test, AMS 11]
theorem a_65 : A 65 := ⊢ A 65
refine ⟨?_, ⊢ 1 < 65 All goals completed! 🐙, ?_, ?_⟩
⊢ ¬Nat.Prime 65 ⊢ ¬Nat.Prime (5 * 13)
exact not_prime_mul (⊢ 5 ≠ 1 All goals completed! 🐙) (⊢ 13 ≠ 1 All goals completed! 🐙)
⊢ φ (65 + 12) = φ 65 + 12 All goals completed! 🐙
⊢ (σ 1) (65 + 12) = (σ 1) 65 + 12 All goals completed! 🐙$209$ is in the sequence A56777.
All goals completed! 🐙
⊢ (σ 1) 221 = (σ 1) 209 + 12 All goals completed! 🐙Numbers coming from prime quadruples are in the sequence A56777.
p:ℕhp:Nat.Prime php2:Nat.Prime (p + 2)hp6:Nat.Prime (p + 6)hp8:Nat.Prime (p + 8)hsum:p * (p + 8) + 12 = (p + 2) * (p + 6)hne_p_p8:p ≠ p + 8hne_p2_p6:p + 2 ≠ p + 6hcop1:p.Coprime (p + 8)hcop2:(p + 2).Coprime (p + 6)e1:(σ 1) p = p + 1e2:(σ 1) (p + 2) = p + 2 + 1e6:(σ 1) (p + 6) = p + 6 + 1e8:(σ 1) (p + 8) = p + 8 + 1⊢ (p + 2 + 1) * (p + 6 + 1) = (p + 1) * (p + 8 + 1) + 12
All goals completed! 🐙$11009$ is in the sequence A56777.
@[category test, AMS 11]
theorem a_11009 : A 11009 := ⊢ A 11009
⊢ ComesFromPrimeQuadruple 11009
exact ⟨101, ⊢ Nat.Prime 101 All goals completed! 🐙, ⊢ Nat.Prime (101 + 2) All goals completed! 🐙, ⊢ Nat.Prime (101 + 6) All goals completed! 🐙, ⊢ Nat.Prime (101 + 8) All goals completed! 🐙, ⊢ 11009 = 101 * (101 + 8) All goals completed! 🐙⟩All members of the sequence A56777 come from prime quadruples.
@[category research open, AMS 11]
theorem comesFromPrimeQuadruple_of_a {n : ℕ} (h : A n) : ComesFromPrimeQuadruple n := n:ℕh:A n⊢ ComesFromPrimeQuadruple n
All goals completed! 🐙Numbers coming from prime quadruples satisfy $n \equiv 65 \pmod{72}$.
p:ℕhp:Nat.Prime php2:Nat.Prime (p + 2)hp6:Nat.Prime (p + 6)hp8:Nat.Prime (p + 8)hp5:5 ≤ ph2✝:¬2 ∣ ph3✝:¬3 ∣ phmod2:p % 2 = 1hmod3:p % 3 = 2hmod6:p % 6 = 5q:ℕ := p / 6hp_eq:p = 6 * q + 5k:ℕhk:q * (q + 3) = 2 * kh1:p * (p + 8) = (6 * q + 5) * (6 * q + 13)h2:(6 * q + 5) * (6 * q + 13) = 36 * (q * (q + 3)) + 65h3:36 * (q * (q + 3)) = 72 * khprod:p * (p + 8) = 72 * k + 65⊢ p * (p + 8) % 72 = 65
All goals completed! 🐙Numbers coming from prime quadruples satisfy $n \equiv 9 \pmod{100}$, except the first value "65".