Dris five-case, odd s: non-square subcase

Open

OddPerfectNumber.no_dris_five_s_ge_two_not_even_nonsq

by ajax · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

divisor-functionnumber-theory

Non-square- $s$ remainder of the Dris $k=5$ , $s\ge 2$ odd leaf.

Preamble

import Mathlib.Tactic

Formal statement

namespace OddPerfectNumber
theorem no_dris_five_s_ge_two_not_even_nonsq (p m s : Nat) (hp : p.Prime) (hp2 : p != 2) (hp4 : p % 4 = 1) (hm : Odd m) (hpm : ¬ p ∣ m) (hs2 : 2 ≤ s) (hs_not_even : ¬ Even s) (hs_nsq : ¬ ∃ r, s = r ^ 2) : ¬ (2 * m ^ 2 = (∑ d ∈ (p ^ 5).divisors, d) * s ∧ (∑ d ∈ (m ^ 2).divisors, d) = p ^ 5 * s) := by sorry
end OddPerfectNumber

Source

https://prove2.me/missions/f37bda44-314b-4d8e-8917-fe26209e0c9c

View graph