Skip to content

Commit 3aeb9ca

Browse files
rwstPaul-LezYaelDillies
authored
feat(OEIS): A000041 (google-deepmind#1704)
Resolves google-deepmind#1494 --------- Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
1 parent a099258 commit 3aeb9ca

File tree

3 files changed

+172
-0
lines changed

3 files changed

+172
-0
lines changed

‎FormalConjectures/OEIS/000041.lean‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
import FormalConjectures.Util.ProblemImports
17+
18+
open Nat
19+
namespace OeisA000041
20+
21+
/-!
22+
Name: "No powers as partition numbers"
23+
24+
There are no partition numbers $p(k)$ of the form $x^m$, with $x,m$ integers $>1$.
25+
26+
*Reference*: [OEIS A000041](https://oeis.org/A000041)
27+
-/
28+
29+
/-- The `n`-th partition number. -/
30+
def p (n : ℕ) : ℕ := Fintype.card (Nat.Partition n)
31+
32+
/--
33+
There are no partition numbers $p(k)$ of the form $x^m$, with $x,m$ integers $>1$.
34+
See comment by Zhi-Wei Sun (Dec 02 2013).
35+
-/
36+
@[category research open, AMS 11]
37+
theorem noPowerPartitionNumber (k : ℕ) : answer(sorry) ↔ ¬IsPerfectPower (p k) := by
38+
sorry
39+
40+
end OeisA000041

‎FormalConjecturesForMathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ import FormalConjecturesForMathlib.Data.Nat.Factorization.Basic
4848
import FormalConjecturesForMathlib.Data.Nat.Full
4949
import FormalConjecturesForMathlib.Data.Nat.Init
5050
import FormalConjecturesForMathlib.Data.Nat.MaxPrimeFac
51+
import FormalConjecturesForMathlib.Data.Nat.PerfectPower
5152
import FormalConjecturesForMathlib.Data.Nat.Prime.Composite
5253
import FormalConjecturesForMathlib.Data.Nat.Prime.Defs
5354
import FormalConjecturesForMathlib.Data.Nat.Prime.Finset

‎FormalConjecturesForMathlib/Data/Nat/PerfectPower.lean‎

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
/-
2+
Copyright 2026 The Formal Conjectures Authors.
3+
4+
Licensed under the Apache License, Version 2.0 (the "License");
5+
you may not use this file except in compliance with the License.
6+
You may obtain a copy of the License at
7+
8+
https://www.apache.org/licenses/LICENSE-2.0
9+
10+
Unless required by applicable law or agreed to in writing, software
11+
distributed under the License is distributed on an "AS IS" BASIS,
12+
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13+
See the License for the specific language governing permissions and
14+
limitations under the License.
15+
-/
16+
import Mathlib.Tactic
17+
18+
namespace Nat
19+
20+
/--
21+
A [perfect power](https://en.wikipedia.org/wiki/Perfect_power) is a natural number that
22+
is a product of equal natural factors, or, in other words, an integer that can be expressed
23+
as a square or a higher integer power of another integer greater than one. More formally,
24+
$n$ is a perfect power if there exist natural numbers $m > 1$, and $k > 1$ such that
25+
$m ^ k = n$. In this case, $n$ may be called a perfect $k$th power. If $k = 2$ or
26+
$k = 3$, then $n$ is called a perfect square or perfect cube, respectively.
27+
-/
28+
def IsPerfectPower (n : ℕ) : Prop :=
29+
∃ k m : ℕ, 1 < k ∧ 1 < m ∧ k ^ m = n
30+
31+
theorem isPerfectPower_iff_factorization_gcd (n : ℕ) :
32+
IsPerfectPower n ↔ n > 1 ∧ n.primeFactors.gcd n.factorization > 1 := by
33+
constructor
34+
· -- Forward direction: IsPerfectPower n → n > 1 ∧ gcd > 1
35+
intro ⟨k, m, hk, hm, hpow⟩
36+
constructor
37+
· -- n > 1
38+
have h : n ≥ 4 := by
39+
calc n = k ^ m := hpow.symm
40+
_ ≥ 2 ^ m := Nat.pow_le_pow_left hk m
41+
_ ≥ 2 ^ 2 := Nat.pow_le_pow_right (by norm_num : 1 ≤ 2) hm
42+
omega
43+
· -- gcd > 1
44+
subst hpow
45+
have hk_pos : k ≠ 0 := Nat.one_le_iff_ne_zero.mp (le_of_lt hk)
46+
have hm_pos : m ≠ 0 := Nat.one_le_iff_ne_zero.mp (le_of_lt hm)
47+
rw [Nat.factorization_pow, primeFactors_pow k hm_pos]
48+
-- m divides every exponent, so gcd ≥ m > 1
49+
have h_nonempty := nonempty_primeFactors.mpr hk
50+
obtain ⟨p, hp⟩ := h_nonempty
51+
-- Show m divides the gcd
52+
have h_m_dvd_gcd : m ∣ k.primeFactors.gcd (m • k.factorization) := by
53+
apply Finset.dvd_gcd
54+
intro b _
55+
show m ∣ (m • k.factorization) b
56+
simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul]
57+
exact dvd_mul_right m _
58+
-- The gcd is positive because k has at least one prime factor with positive exponent
59+
have hp_in_support : p ∈ k.factorization.support := by
60+
rw [support_factorization]; exact hp
61+
have hp_exp_pos : 0 < k.factorization p := Finsupp.mem_support_iff.mp hp_in_support |> Nat.pos_of_ne_zero
62+
have h_gcd_pos : 0 < k.primeFactors.gcd (m • k.factorization) := by
63+
have h1 := Finset.gcd_dvd (f := (m • k.factorization)) hp
64+
have h_eq : (m • k.factorization) p = m * k.factorization p := by
65+
simp only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul]
66+
rw [h_eq] at h1
67+
have h_val_pos : 0 < m * k.factorization p := Nat.mul_pos (Nat.pos_of_ne_zero hm_pos) hp_exp_pos
68+
exact Nat.pos_of_dvd_of_pos h1 h_val_pos
69+
exact Nat.lt_of_lt_of_le hm (Nat.le_of_dvd h_gcd_pos h_m_dvd_gcd)
70+
· -- Backward direction: n > 1 ∧ gcd > 1 → IsPerfectPower n
71+
intro ⟨hn, hgcd⟩
72+
set g := n.primeFactors.gcd n.factorization with hg_def
73+
-- Define k as the product of p^(n.factorization p / g) for all primes p | n
74+
let f : ℕ → ℕ := fun q => q ^ (n.factorization q / g)
75+
set k := n.primeFactors.prod f with hk_def
76+
use k, g
77+
refine ⟨?_, hgcd, ?_⟩
78+
· -- k > 1
79+
have h_nonempty := nonempty_primeFactors.mpr hn
80+
obtain ⟨p, hp⟩ := h_nonempty
81+
have hp_prime := prime_of_mem_primeFactors hp
82+
-- p ∈ n.primeFactors means n.factorization p > 0
83+
have hp_in_support : p ∈ n.factorization.support := by
84+
rw [support_factorization]; exact hp
85+
have hp_pos : 0 < n.factorization p := Finsupp.mem_support_iff.mp hp_in_support |> Nat.pos_of_ne_zero
86+
have h_div : g ∣ n.factorization p := Finset.gcd_dvd hp
87+
have hg_pos : 0 < g := Nat.lt_trans Nat.zero_lt_one hgcd
88+
have h_quot_pos : 0 < n.factorization p / g :=
89+
Nat.div_pos (Nat.le_of_dvd hp_pos h_div) hg_pos
90+
have h_ge_p : k ≥ f p := by
91+
rw [hk_def]
92+
exact Finset.single_le_prod' (f := f)
93+
(fun q hq => Nat.one_le_pow _ _ (Prime.one_le (prime_of_mem_primeFactors hq))) hp
94+
have h_ge_2 : f p ≥ 2 := by
95+
show p ^ (n.factorization p / g) ≥ 2
96+
calc p ^ (n.factorization p / g) ≥ p ^ 1 := Nat.pow_le_pow_right (Prime.one_le hp_prime) h_quot_pos
97+
_ = p := pow_one p
98+
_ ≥ 2 := Prime.two_le hp_prime
99+
omega
100+
· -- k ^ g = n
101+
have h_eq : k ^ g = n.primeFactors.prod (fun q => q ^ (n.factorization q / g * g)) := by
102+
rw [hk_def, ← Finset.prod_pow]
103+
congr 1
104+
ext q
105+
show (f q) ^ g = q ^ (n.factorization q / g * g)
106+
simp only [f, ← pow_mul]
107+
rw [h_eq]
108+
have hn_ne_zero : n ≠ 0 := Nat.ne_of_gt (Nat.lt_of_succ_lt hn)
109+
conv_rhs => rw [← Nat.factorization_prod_pow_eq_self hn_ne_zero]
110+
congr 1
111+
ext p
112+
by_cases hp : p ∈ n.primeFactors
113+
· have h_div : g ∣ n.factorization p := Finset.gcd_dvd hp
114+
rw [Nat.div_mul_cancel h_div]
115+
· -- p ∉ n.primeFactors means n.factorization p = 0
116+
have hp_not_in_support : p ∉ n.factorization.support := by
117+
rw [support_factorization]; exact hp
118+
have hp_zero : n.factorization p = 0 := Finsupp.notMem_support_iff.mp hp_not_in_support
119+
simp only [hp_zero, Nat.zero_div, zero_mul, pow_zero]
120+
121+
instance IsPerfectPower.decide : ∀ n, Decidable (IsPerfectPower n) := fun n =>
122+
decidable_of_iff (n > 1 ∧ n.primeFactors.gcd n.factorization > 1)
123+
(isPerfectPower_iff_factorization_gcd n).symm
124+
125+
example : IsPerfectPower 4 := by native_decide
126+
example : IsPerfectPower 27 := by native_decide
127+
example : ¬IsPerfectPower 0 := by native_decide
128+
example : ¬IsPerfectPower 1 := by native_decide
129+
example : ¬IsPerfectPower 2 := by native_decide
130+
131+
end Nat

0 commit comments

Comments
 (0)