/-
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 FormalConjecturesUtilCuban Primes
OEIS A002407 lists the primes that are differences of two consecutive positive cubes. The sequence is conjectured to be infinite.
References:
namespace OeisA2407
A natural number is in A002407 when it is prime and is the difference of two consecutive
positive cubes. The addition equality avoids truncated subtraction in ℕ.
def A (p : ℕ) : Prop :=
p.Prime ∧ ∃ k > 0, p + k ^ 3 = (k + 1) ^ 3@[category test, AMS 11]
theorem a_7 : A 7 := ⊢ A 7
refine ⟨⊢ Nat.Prime 7 All goals completed! 🐙, 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ 7 + 1 ^ 3 = (1 + 1) ^ 3 All goals completed! 🐙⟩@[category test, AMS 11]
theorem a_19 : A 19 := ⊢ A 19
refine ⟨⊢ Nat.Prime 19 All goals completed! 🐙, 2, ⊢ 2 > 0 All goals completed! 🐙, ⊢ 19 + 2 ^ 3 = (2 + 1) ^ 3 All goals completed! 🐙⟩@[category test, AMS 11]
theorem a_37 : A 37 := ⊢ A 37
refine ⟨⊢ Nat.Prime 37 All goals completed! 🐙, 3, ⊢ 3 > 0 All goals completed! 🐙, ⊢ 37 + 3 ^ 3 = (3 + 1) ^ 3 All goals completed! 🐙⟩@[category test, AMS 11]
theorem a_61 : A 61 := ⊢ A 61
refine ⟨⊢ Nat.Prime 61 All goals completed! 🐙, 4, ⊢ 4 > 0 All goals completed! 🐙, ⊢ 61 + 4 ^ 3 = (4 + 1) ^ 3 All goals completed! 🐙⟩@[category test, AMS 11]
theorem a_127 : A 127 := ⊢ A 127
refine ⟨⊢ Nat.Prime 127 All goals completed! 🐙, 6, ⊢ 6 > 0 All goals completed! 🐙, ⊢ 127 + 6 ^ 3 = (6 + 1) ^ 3 All goals completed! 🐙⟩@[category test, AMS 11]
theorem not_a_91 : ¬ A 91 := ⊢ ¬A 91
All goals completed! 🐙This sequence is believed to be infinite.
@[category research open, AMS 11]
theorem conjecture : {p : ℕ | A p}.Infinite := ⊢ {p | A p}.Infinite
All goals completed! 🐙end OeisA2407