Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Every prime dividing the k=5 index divides the cyclotomic product

Disproved
OddPerfectNumber.Kernel.five_two_prime_index_dvd

by WillR · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

Let p be a prime congruent to 1 modulo 4, m an odd natural number not divisible by p, and q and r primes. Suppose the k=5 Dris equation 2 m squared equals sigma of p to the fifth times d1 squared q r in its already factorised form. Then every prime dividing the index d1 squared q r also divides the cyclotomic product (p+1)/2 times p squared plus p plus one times p squared minus p plus one. Equivalently, the squarefree kernel of that cyclotomic product is contained in the set of primes dividing the index. Since the index has squarefree kernel exactly the two primes q and r, this forces the squarefree kernel of the cyclotomic product to have at most two prime factors, which for all but two Euler primes up to fifteen hundred fails.

Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel

theorem five_two_prime_index_dvd {p m d1 q r : Nat} (hp : p.Prime)
    (hp2 : p != 2) (hp4 : p % 4 = 1) (hm : Odd m) (hpm : ¬ p ∣ m)
    (hq : q.Prime) (hr : r.Prime)
    (h1 : 2 * m ^ 2 =
      (2 * (p ^ 2 + p + 1) * ((p + 1) / 2 * (p ^ 2 - p + 1))) * (d1 ^ 2 * (q * r)))
    (hm0 : m != 0) :
    ∀ t, Dvd.dvd t (d1 ^ 2 * (q * r)) ->
      Dvd.dvd t ((p + 1) / 2 * (p ^ 2 + p + 1) * (p ^ 2 - p + 1)) := by
  sorry

end OddPerfectNumber.Kernel

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me