FormalConjectures.OEIS.«108864»

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

Numbers $n$ such that the perfect deficiency of $n$ is $\le 10$.

We formally define the property satisfied by elements of the sequence, using the sum of divisors function $\sigma_1(n)$.

References:

A108864

namespace OeisA108864open Nat Finset Int

The condition for a number $n$ to be in the sequence. It satisfies $0 < n$ and its perfect deficiency is $\le 10$, using the sum of divisors function $\sigma_1(n)$.

def A (n : ℕ) : Prop :=
  let sigmaOneN : ℕ := (Nat.divisors n).sum id
  0 < n ∧ ((sigmaOneN : ℤ) - 2 * (n : ℤ)).natAbs ≤ 10

instance : DecidablePred A := by⊢ DecidablePred A
  unfold A⊢ DecidablePred fun n ↦
  have sigmaOneN := n.divisors.sum id;
  0 < n ∧ (↑sigmaOneN - 2 * ↑n).natAbs ≤ 10
  infer_instanceAll goals completed! 🐙

The primary defining sequence a. a n is the n-th number (0-indexed) such that its perfect deficiency is $\le 10$.

noncomputable def a (n : ℕ) : ℕ :=
  n.nth A

Term theorems verifying the first few values of the sequence against the official OEIS b-file


@[category test, AMS 11]
theorem a_0 : a 0 = 1 := by⊢ a 0 = 1
  have h1 : A 1 := by decideh1:A 1⊢ a 0 = 1h1:A 1⊢ a 0 = 1
  have hcnt : Nat.count A 1 = 0 := by decideh1:A 1hcnt:count A 1 = 0⊢ a 0 = 1h1:A 1hcnt:count A 1 = 0⊢ a 0 = 1
  have := Nat.nth_count (p := A) h1h1:A 1hcnt:count A 1 = 0this:nth A (count A 1) = 1⊢ a 0 = 1
  rwa [hcnth1:A 1hcnt:count A 1 = 0this:nth A 0 = 1⊢ a 0 = 1]h1:A 1hcnt:count A 1 = 0this:nth A 0 = 1⊢ a 0 = 1 at this



@[category test, AMS 11]
theorem a_1 : a 1 = 2 := by⊢ a 1 = 2
  have h2 : A 2 := by decideh2:A 2⊢ a 1 = 2h2:A 2⊢ a 1 = 2
  have hcnt : Nat.count A 2 = 1 := by decideh2:A 2hcnt:count A 2 = 1⊢ a 1 = 2h2:A 2hcnt:count A 2 = 1⊢ a 1 = 2
  have := Nat.nth_count (p := A) h2h2:A 2hcnt:count A 2 = 1this:nth A (count A 2) = 2⊢ a 1 = 2
  rwa [hcnth2:A 2hcnt:count A 2 = 1this:nth A 1 = 2⊢ a 1 = 2]h2:A 2hcnt:count A 2 = 1this:nth A 1 = 2⊢ a 1 = 2 at this



@[category test, AMS 11]
theorem a_2 : a 2 = 3 := by⊢ a 2 = 3
  have h3 : A 3 := by decideh3:A 3⊢ a 2 = 3h3:A 3⊢ a 2 = 3
  have hcnt : Nat.count A 3 = 2 := by decideh3:A 3hcnt:count A 3 = 2⊢ a 2 = 3h3:A 3hcnt:count A 3 = 2⊢ a 2 = 3
  have := Nat.nth_count (p := A) h3h3:A 3hcnt:count A 3 = 2this:nth A (count A 3) = 3⊢ a 2 = 3
  rwa [hcnth3:A 3hcnt:count A 3 = 2this:nth A 2 = 3⊢ a 2 = 3]h3:A 3hcnt:count A 3 = 2this:nth A 2 = 3⊢ a 2 = 3 at this



@[category test, AMS 11]
theorem a_3 : a 3 = 4 := by⊢ a 3 = 4
  have h4 : A 4 := by decideh4:A 4⊢ a 3 = 4h4:A 4⊢ a 3 = 4
  have hcnt : Nat.count A 4 = 3 := by decideh4:A 4hcnt:count A 4 = 3⊢ a 3 = 4h4:A 4hcnt:count A 4 = 3⊢ a 3 = 4
  have := Nat.nth_count (p := A) h4h4:A 4hcnt:count A 4 = 3this:nth A (count A 4) = 4⊢ a 3 = 4
  rwa [hcnth4:A 4hcnt:count A 4 = 3this:nth A 3 = 4⊢ a 3 = 4]h4:A 4hcnt:count A 4 = 3this:nth A 3 = 4⊢ a 3 = 4 at this



@[category test, AMS 11]
theorem a_4 : a 4 = 5 := by⊢ a 4 = 5
  have h5 : A 5 := by decideh5:A 5⊢ a 4 = 5h5:A 5⊢ a 4 = 5
  have hcnt : Nat.count A 5 = 4 := by decideh5:A 5hcnt:count A 5 = 4⊢ a 4 = 5h5:A 5hcnt:count A 5 = 4⊢ a 4 = 5
  have := Nat.nth_count (p := A) h5h5:A 5hcnt:count A 5 = 4this:nth A (count A 5) = 5⊢ a 4 = 5
  rwa [hcnth5:A 5hcnt:count A 5 = 4this:nth A 4 = 5⊢ a 4 = 5]h5:A 5hcnt:count A 5 = 4this:nth A 4 = 5⊢ a 4 = 5 at this

Is 1155 the last odd number in this sequence? (1155 is the 59th term starting from 1, corresponding to a 58 = 1155).

@[category research open, AMS 11]
theorem conjecture :
    answer(sorry) ↔ ∀ n > 58, Even (a n) := by⊢ True ↔ ∀ n > 58, Even (OeisA108864.a n)
  sorryAll goals completed! 🐙

end OeisA108864