FormalConjectures.OEIS.«84046»

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

Smallest prime $p$ such that $p + n$ is an $n$-th power

Smallest prime $p$ such that $p + n$ is an $n$-th power, or $0$ if no such number exists. That is, the smallest prime of the form $k^n - n$.

References:

A084046

namespace OeisA84046

Smallest prime $p$ such that $p + n$ is an $n$-th power, or $0$ if no such prime exists.

noncomputable def a (n : ℕ) : ℕ :=
  sInf {p : ℕ | p.Prime ∧ ∃ k : ℕ, k ^ n = p + n}

Value of the sequence a at 0.


@[category test, AMS 11]
theorem a_0 : a 0 = 0 := by⊢ a 0 = 0
  change sInf {p : ℕ | p.Prime ∧ ∃ k : ℕ, k ^ 0 = p + 0} = 0⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0
  have h_empty : {p : ℕ | p.Prime ∧ ∃ k : ℕ, k ^ 0 = p + 0} = ∅ := by⊢ a 0 = 0h_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0
    ext pp:ℕ⊢ p ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} ↔ p ∈ ∅h_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0
    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false, not_and]p:ℕ⊢ Nat.Prime p → ¬∃ k, k ^ 0 = p + 0h_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0
    intro hp ⟨k, hk⟩p:ℕhp:Nat.Prime pk:ℕhk:k ^ 0 = p + 0⊢ Falseh_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0
    rw [pow_zero,p:ℕhp:Nat.Prime pk:ℕhk:1 = p + 0⊢ Falsep:ℕhp:Nat.Prime pk:ℕhk:1 = p⊢ Falseh_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0 add_zerop:ℕhp:Nat.Prime pk:ℕhk:1 = p⊢ Falsep:ℕhp:Nat.Prime pk:ℕhk:1 = p⊢ Falseh_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0] at hkp:ℕhp:Nat.Prime pk:ℕhk:1 = p⊢ Falseh_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0
    subst hkk:ℕhp:Nat.Prime 1⊢ Falseh_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0
    exact Nat.not_prime_one hph_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0h_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf {p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = 0
  rw [h_empty,h_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ sInf ∅ = 0All goals completed! 🐙 Nat.sInf_emptyh_empty:{p | Nat.Prime p ∧ ∃ k, k ^ 0 = p + 0} = ∅⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

Value of the sequence a at 1.


@[category test, AMS 11]
theorem a_1 : a 1 = 2 := by⊢ a 1 = 2
  have h_least : IsLeast {p : ℕ | p.Prime ∧ ∃ k : ℕ, k ^ 1 = p + 1} 2 := by
    constructorleft⊢ 2 ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1}right⊢ 2 ∈ lowerBounds {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2
    ·left⊢ 2 ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2 simp only [Set.mem_ofPred_eq]left⊢ Nat.Prime 2 ∧ ∃ k, k ^ 1 = 2 + 1h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2
      refine ⟨Nat.prime_two, 3, by⊢ 3 ^ 1 = 2 + 1h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2 norm_numAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2⟩
    ·right⊢ 2 ∈ lowerBounds {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2 intro p hprightp:ℕhp:p ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1}⊢ 2 ≤ ph_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2
      simp only [Set.mem_ofPred_eq] at hprightp:ℕhp:Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1⊢ 2 ≤ ph_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2
      exact hp.1.two_leh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 1 = p + 1} 2⊢ a 1 = 2
  exact h_least.csInf_eqAll goals completed! 🐙

Value of the sequence a at 2.


@[category test, AMS 11]
theorem a_2 : a 2 = 2 := by⊢ a 2 = 2
  have h_least : IsLeast {p : ℕ | p.Prime ∧ ∃ k : ℕ, k ^ 2 = p + 2} 2 := by
    constructorleft⊢ 2 ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2}right⊢ 2 ∈ lowerBounds {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2
    ·left⊢ 2 ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2 simp only [Set.mem_ofPred_eq]left⊢ Nat.Prime 2 ∧ ∃ k, k ^ 2 = 2 + 2h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2
      refine ⟨Nat.prime_two, 2, by⊢ 2 ^ 2 = 2 + 2h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2 norm_numAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2⟩
    ·right⊢ 2 ∈ lowerBounds {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2 intro p hprightp:ℕhp:p ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2}⊢ 2 ≤ ph_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2
      simp only [Set.mem_ofPred_eq] at hprightp:ℕhp:Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2⊢ 2 ≤ ph_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2
      exact hp.1.two_leh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 2 = p + 2} 2⊢ a 2 = 2
  exact h_least.csInf_eqAll goals completed! 🐙

Value of the sequence a at 3.


@[category test, AMS 11]
theorem a_3 : a 3 = 5 := by⊢ a 3 = 5
  have h_least : IsLeast {p : ℕ | p.Prime ∧ ∃ k : ℕ, k ^ 3 = p + 3} 5 := by
    constructorleft⊢ 5 ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3}right⊢ 5 ∈ lowerBounds {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
    ·left⊢ 5 ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 simp only [Set.mem_ofPred_eq]left⊢ Nat.Prime 5 ∧ ∃ k, k ^ 3 = 5 + 3h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      refine ⟨by⊢ Nat.Prime 5h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 norm_numAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5, 2, by⊢ 2 ^ 3 = 5 + 3h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 norm_numAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5⟩
    ·right⊢ 5 ∈ lowerBounds {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3}h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 intro p hprightp:ℕhp:p ∈ {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3}⊢ 5 ≤ ph_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      simp only [Set.mem_ofPred_eq] at hprightp:ℕhp:Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3⊢ 5 ≤ ph_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      rcases hp with ⟨hp_prime, k, hk⟩rightp:ℕhp_prime:Nat.Prime pk:ℕhk:k ^ 3 = p + 3⊢ 5 ≤ ph_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      by_contra! hrightp:ℕhp_prime:Nat.Prime pk:ℕhk:k ^ 3 = p + 3h:p < 5⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      interval_cases pright.«0»p:ℕk:ℕhp_prime:Nat.Prime 0hk:k ^ 3 = 0 + 3h:0 < 5⊢ Falseright.«1»p:ℕk:ℕhp_prime:Nat.Prime 1hk:k ^ 3 = 1 + 3h:1 < 5⊢ Falseright.«2»p:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5⊢ Falseright.«3»p:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5⊢ Falseright.«4»p:ℕk:ℕhp_prime:Nat.Prime 4hk:k ^ 3 = 4 + 3h:4 < 5⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      ·right.«0»p:ℕk:ℕhp_prime:Nat.Prime 0hk:k ^ 3 = 0 + 3h:0 < 5⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 exact Nat.not_prime_zero hp_primeAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      ·right.«1»p:ℕk:ℕhp_prime:Nat.Prime 1hk:k ^ 3 = 1 + 3h:1 < 5⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 exact Nat.not_prime_one hp_primeAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      ·right.«2»p:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 rcases (show k ≤ 1 ∨ 2 ≤ k by omegaAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5) with hk_le | hk_ge
        ·right.«2».inlp:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5hk_le:k ≤ 1⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 interval_cases kright.«2».inl.«0»p:ℕk:ℕhp_prime:Nat.Prime 2h:2 < 5hk:0 ^ 3 = 2 + 3hk_le:0 ≤ 1⊢ Falseright.«2».inl.«1»p:ℕk:ℕhp_prime:Nat.Prime 2h:2 < 5hk:1 ^ 3 = 2 + 3hk_le:1 ≤ 1⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 <;>right.«2».inl.«0»p:ℕk:ℕhp_prime:Nat.Prime 2h:2 < 5hk:0 ^ 3 = 2 + 3hk_le:0 ≤ 1⊢ Falseright.«2».inl.«1»p:ℕk:ℕhp_prime:Nat.Prime 2h:2 < 5hk:1 ^ 3 = 2 + 3hk_le:1 ≤ 1⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 revert hkright.«2».inl.«1»p:ℕk:ℕhp_prime:Nat.Prime 2h:2 < 5hk_le:1 ≤ 1⊢ 1 ^ 3 = 2 + 3 → Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 <;>right.«2».inl.«0»p:ℕk:ℕhp_prime:Nat.Prime 2h:2 < 5hk_le:0 ≤ 1⊢ 0 ^ 3 = 2 + 3 → Falseright.«2».inl.«1»p:ℕk:ℕhp_prime:Nat.Prime 2h:2 < 5hk_le:1 ≤ 1⊢ 1 ^ 3 = 2 + 3 → Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 decideAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
        ·right.«2».inrp:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5hk_ge:2 ≤ k⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 have : 8 ≤ k ^ 3 := by⊢ a 3 = 5right.«2».inrp:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5hk_ge:2 ≤ kthis:8 ≤ k ^ 3⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
            calc 8 = 2 ^ 3 := byp:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5hk_ge:2 ≤ k⊢ 8 = 2 ^ 3right.«2».inrp:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5hk_ge:2 ≤ kthis:8 ≤ k ^ 3⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 decideAll goals completed! 🐙right.«2».inrp:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5hk_ge:2 ≤ kthis:8 ≤ k ^ 3⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
            _ ≤ k ^ 3 := Nat.pow_le_pow_left hk_ge 3right.«2».inrp:ℕk:ℕhp_prime:Nat.Prime 2hk:k ^ 3 = 2 + 3h:2 < 5hk_ge:2 ≤ kthis:8 ≤ k ^ 3⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
          omegaAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      ·right.«3»p:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 rcases (show k ≤ 1 ∨ 2 ≤ k by omegaAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5) with hk_le | hk_ge
        ·right.«3».inlp:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5hk_le:k ≤ 1⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 interval_cases kright.«3».inl.«0»p:ℕk:ℕhp_prime:Nat.Prime 3h:3 < 5hk:0 ^ 3 = 3 + 3hk_le:0 ≤ 1⊢ Falseright.«3».inl.«1»p:ℕk:ℕhp_prime:Nat.Prime 3h:3 < 5hk:1 ^ 3 = 3 + 3hk_le:1 ≤ 1⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 <;>right.«3».inl.«0»p:ℕk:ℕhp_prime:Nat.Prime 3h:3 < 5hk:0 ^ 3 = 3 + 3hk_le:0 ≤ 1⊢ Falseright.«3».inl.«1»p:ℕk:ℕhp_prime:Nat.Prime 3h:3 < 5hk:1 ^ 3 = 3 + 3hk_le:1 ≤ 1⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 revert hkright.«3».inl.«1»p:ℕk:ℕhp_prime:Nat.Prime 3h:3 < 5hk_le:1 ≤ 1⊢ 1 ^ 3 = 3 + 3 → Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 <;>right.«3».inl.«0»p:ℕk:ℕhp_prime:Nat.Prime 3h:3 < 5hk_le:0 ≤ 1⊢ 0 ^ 3 = 3 + 3 → Falseright.«3».inl.«1»p:ℕk:ℕhp_prime:Nat.Prime 3h:3 < 5hk_le:1 ≤ 1⊢ 1 ^ 3 = 3 + 3 → Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 decideAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
        ·right.«3».inrp:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5hk_ge:2 ≤ k⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 have : 8 ≤ k ^ 3 := by⊢ a 3 = 5right.«3».inrp:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5hk_ge:2 ≤ kthis:8 ≤ k ^ 3⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
            calc 8 = 2 ^ 3 := byp:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5hk_ge:2 ≤ k⊢ 8 = 2 ^ 3right.«3».inrp:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5hk_ge:2 ≤ kthis:8 ≤ k ^ 3⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 decideAll goals completed! 🐙right.«3».inrp:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5hk_ge:2 ≤ kthis:8 ≤ k ^ 3⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
            _ ≤ k ^ 3 := Nat.pow_le_pow_left hk_ge 3right.«3».inrp:ℕk:ℕhp_prime:Nat.Prime 3hk:k ^ 3 = 3 + 3h:3 < 5hk_ge:2 ≤ kthis:8 ≤ k ^ 3⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
          omegaAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
      ·right.«4»p:ℕk:ℕhp_prime:Nat.Prime 4hk:k ^ 3 = 4 + 3h:4 < 5⊢ Falseh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 exact (byp:ℕk:ℕhp_prime:Nat.Prime 4hk:k ^ 3 = 4 + 3h:4 < 5⊢ ¬Nat.Prime 4h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 decideAll goals completed! 🐙h_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5 : ¬ Nat.Prime 4) hp_primeh_least:IsLeast {p | Nat.Prime p ∧ ∃ k, k ^ 3 = p + 3} 5⊢ a 3 = 5
  exact h_least.csInf_eqAll goals completed! 🐙

Conjecture: if a(k) = 0 then k is an even square.

@[category research open, AMS 11]
theorem conjecture (k : ℕ) (h : a k = 0) : ∃ m : ℕ, k = (2 * m) ^ 2 := byk:ℕh:a k = 0⊢ ∃ m, k = (2 * m) ^ 2
  sorryAll goals completed! 🐙

end OeisA84046