Likely misformalization in `OEIS/108864.lean`

[tadamcz]

An AI agent produced a Lean proof of the negation of OeisA108864.conjecture for about
$0.41 of API spend, which is unrealistically low for a research-open conjecture from the
OEIS set.

AI review of the accepted proof suggests the statement is misformalized, in the following way (AI-written):

The defect is in the file's membership predicate:

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

A108864 is "numbers n such that the perfect deficiency of n
(A109883) is <= 10", where A109883 is the remainder after greedily
subtracting the divisors of n in increasing order. The file substitutes |σ₁(n) − 2n| ≤ 10,
which is a different function, and the two sets diverge in both directions: 24 is a member of
the real sequence (its perfect deficiency is 0) but |σ(24) − 48| = 12 excludes it here, while
56 satisfies |σ(56) − 112| = 8 and is included here despite having perfect deficiency 20.

The conjecture ("Is 1155 the last odd number in this sequence?", rendered as
∀ n > 58, Even (a n)) therefore quantifies over the wrong sequence. The accepted disproof
kernel-certifies an odd member of the formal set at an index above 58, namely
442365 = 3 · 5 · 7 · 11 · 383 (with σ − 2n = 6); under the true greedy definition its perfect
deficiency is 147449, so it is not in A108864 at all, and the OEIS question is untouched.

Suggested fix: define membership through A109883's greedy divisor-subtraction remainder rather
than through σ₁(n) − 2n.

The accepted Lean proof

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](https://oeis.org/A108864)
-/

namespace OeisA108864

open 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
  unfold A
  infer_instance

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

/-- An explicit collection of 59 members preceding the counterexample. -/
private def earlierTerms : Finset ℕ :=
  {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 15, 16, 18, 20, 21, 22, 26,
   28, 32, 40, 44, 50, 52, 56, 64, 68, 70, 88, 104, 110, 128, 130, 136, 152,
   184, 196, 256, 315, 368, 464, 496, 512, 592, 650, 656, 836, 884, 1012,
   1024, 1155, 1696, 1888, 1952, 2048, 2144, 2272}

set_option maxRecDepth 10000 in
set_option maxHeartbeats 2000000 in
/--
The odd number `442365 = 1155 * 383` has divisor sum `884736`, so its
perfect deficiency has absolute value 6. There are at least 59 members
of the sequence below it, contradicting the proposed parity assertion.
-/
theorem conjecture.disproof :
    ¬ (∀ n > 58, Even (a n)) := by
  have hsum : (Nat.divisors 442365).sum id = 884736 := by
    change (Nat.divisors (1155 * 383)).sum (fun d => d) = _
    rw [Nat.Coprime.sum_divisors_mul (by norm_num : Nat.Coprime 1155 383)]
    rw [Nat.Prime.divisors (by norm_num : Nat.Prime 383)]
    have hsmall : (Nat.divisors 1155).sum (fun d => d) = 2304 := by decide
    rw [hsmall]
    norm_num
  have hmem : A 442365 := by
    unfold A
    rw [hsum]
    norm_num
  have hcard : earlierTerms.card = 59 := by decide
  have hearlier : ∀ m ∈ earlierTerms, m < 442365 ∧ A m := by decide +kernel
  have hcount : 59 ≤ Nat.count A 442365 := by
    rw [Nat.count_eq_card_filter_range, ← hcard]
    apply Finset.card_le_card
    intro m hm
    exact Finset.mem_filter.mpr
      ⟨Finset.mem_range.mpr (hearlier m hm).1, (hearlier m hm).2⟩
  have hnth : a (Nat.count A 442365) = 442365 := Nat.nth_count hmem
  intro h
  have heven := h (Nat.count A 442365) (by omega)
  rw [hnth] at heven
  norm_num at heven

end OeisA108864