/-
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 FormalConjecturesUtilPractical numbers
A positive integer $n$ is called a practical number (or panarithmic number) if every positive integer $m \le n$ can be represented as a sum of distinct divisors of $n$.
References:
namespace OeisA5153A positive integer $n$ is practical if every $m \le n$ can be represented as a sum of distinct divisors of $n$.
def A (n : ℕ) : Prop :=
0 < n ∧ Nat.IsPractical n$1$ is a practical number.
@[category test, AMS 11]
theorem a_1 : A 1 := ⊢ A 1
refine ⟨⊢ 0 < 1 All goals completed! 🐙, fun m hm => ?_⟩
m:ℕhm:0 ≤ 1⊢ 0 ∈ subsetSums ↑(Nat.divisors 1)m:ℕhm:1 ≤ 1⊢ 1 ∈ subsetSums ↑(Nat.divisors 1)
m:ℕhm:0 ≤ 1⊢ 0 ∈ subsetSums ↑(Nat.divisors 1) exact ⟨∅, m:ℕhm:0 ≤ 1⊢ ↑∅ ⊆ ↑(Nat.divisors 1) All goals completed! 🐙, m:ℕhm:0 ≤ 1⊢ 0 = ∑ i ∈ ∅, i All goals completed! 🐙⟩
m:ℕhm:1 ≤ 1⊢ 1 ∈ subsetSums ↑(Nat.divisors 1) exact ⟨{1}, m:ℕhm:1 ≤ 1⊢ ↑{1} ⊆ ↑(Nat.divisors 1) All goals completed! 🐙, m:ℕhm:1 ≤ 1⊢ 1 = ∑ i ∈ {1}, i All goals completed! 🐙⟩$2$ is a practical number.
@[category test, AMS 11]
theorem a_2 : A 2 := ⊢ A 2
refine ⟨⊢ 0 < 2 All goals completed! 🐙, fun m hm => ?_⟩
m:ℕhm:0 ≤ 2⊢ 0 ∈ subsetSums ↑(Nat.divisors 2)m:ℕhm:1 ≤ 2⊢ 1 ∈ subsetSums ↑(Nat.divisors 2)m:ℕhm:2 ≤ 2⊢ 2 ∈ subsetSums ↑(Nat.divisors 2)
m:ℕhm:0 ≤ 2⊢ 0 ∈ subsetSums ↑(Nat.divisors 2) exact ⟨∅, m:ℕhm:0 ≤ 2⊢ ↑∅ ⊆ ↑(Nat.divisors 2) All goals completed! 🐙, m:ℕhm:0 ≤ 2⊢ 0 = ∑ i ∈ ∅, i All goals completed! 🐙⟩
m:ℕhm:1 ≤ 2⊢ 1 ∈ subsetSums ↑(Nat.divisors 2) exact ⟨{1}, m:ℕhm:1 ≤ 2⊢ ↑{1} ⊆ ↑(Nat.divisors 2) All goals completed! 🐙, m:ℕhm:1 ≤ 2⊢ 1 = ∑ i ∈ {1}, i All goals completed! 🐙⟩
m:ℕhm:2 ≤ 2⊢ 2 ∈ subsetSums ↑(Nat.divisors 2) exact ⟨{2}, m:ℕhm:2 ≤ 2⊢ ↑{2} ⊆ ↑(Nat.divisors 2) All goals completed! 🐙, m:ℕhm:2 ≤ 2⊢ 2 = ∑ i ∈ {2}, i All goals completed! 🐙⟩$4$ is a practical number.
m:ℕhd:Nat.divisors 4 = {1, 2, 4}hm:4 ≤ 4⊢ {4} ⊆ {1, 2, 4}; All goals completed! 🐙, m:ℕhd:Nat.divisors 4 = {1, 2, 4}hm:4 ≤ 4⊢ 4 = ∑ i ∈ {4}, i All goals completed! 🐙⟩$6$ is a practical number.
m:ℕhd:Nat.divisors 6 = {1, 2, 3, 6}hm:6 ≤ 6⊢ {6} ⊆ {1, 2, 3, 6}; All goals completed! 🐙, m:ℕhd:Nat.divisors 6 = {1, 2, 3, 6}hm:6 ≤ 6⊢ 6 = ∑ i ∈ {6}, i All goals completed! 🐙⟩$8$ is a practical number.
m:ℕhd:Nat.divisors 8 = {1, 2, 4, 8}hm:8 ≤ 8⊢ {8} ⊆ {1, 2, 4, 8}; All goals completed! 🐙, m:ℕhd:Nat.divisors 8 = {1, 2, 4, 8}hm:8 ≤ 8⊢ 8 = ∑ i ∈ {8}, i All goals completed! 🐙⟩Conjecture: every odd number, beginning with 3, is the sum of a prime number and a practical number.
Hal M. Switkay, Jan 28 2023
@[category research open, AMS 11]
theorem conjecture (n : ℕ) (hn : 3 ≤ n) (hodd : Odd n) :
∃ p q : ℕ, p.Prime ∧ A q ∧ n = p + q := n:ℕhn:3 ≤ nhodd:Odd n⊢ ∃ p q, Nat.Prime p ∧ A q ∧ n = p + q
All goals completed! 🐙end OeisA5153