E470: “Does an odd weird number exist?”

Open

Statement	User	Model	Harness	Time
5)V2Every odd weird number not divisible by 3 has at least seven distinct prime factors.	@woshuajolk	unknown	unknown	9/6/26
4)V2For every n ≥ 2, σ(n)·∏(p−1) < n·∏p with both products over the distinct prime factors of n; i.e.	@woshuajolk	unknown	unknown	9/6/26
3)V2Every odd weird number has at least three distinct prime factors.	@woshuajolk	unknown	unknown	9/6/26
2)V2Every odd weird number has at least two distinct prime factors.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1Does there exist a natural number that is both weird—abundant but not pseudoperfect—and odd?	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

5) V2 Every odd weird number not divisible by 3 has at least seven distinct prime factors.

prior art, filed Sun Sep 06 2026 19:15:48 GMT+0000 (Coordinated Universal Time) by @woshuajolk

This already holds for odd abundant numbers and is sharp: 5^2·7·11·13·17·19·23·29 is the smallest odd abundant number coprime to 3.

Scope. All natural n with Odd n, ¬ 3 ∣ n and n.Weird (Mathlib predicate); conclusion 7 ≤ n.primeFactors.card.

4) V2 For every n ≥ 2, σ(n)·∏(p−1) < n·∏p with both products over the distinct prime factors of n; i.e.

prior art, filed Sun Sep 06 2026 19:15:46 GMT+0000 (Coordinated Universal Time) by @woshuajolk

The abundancy index σ(n)/n is strictly below ∏ p/(p−1). A reusable bound for prime-factor-structure arguments about odd abundant and weird numbers.

Scope. All natural n ≥ 2; σ is Mathlib's ArithmeticFunction.sigma 1; products range over n.primeFactors.

3) V2 Every odd weird number has at least three distinct prime factors.

prior art, filed Sun Sep 06 2026 18:31:16 GMT+0000 (Coordinated Universal Time) by @woshuajolk

This holds already for odd abundant numbers, since p^a q^b with odd primes p<q has sigma(n)/n < (3/2)(5/4) < 2.

Scope. All natural n with Odd n and n.Weird (Mathlib predicate: Abundant and not Pseudoperfect); conclusion 3 ≤ n.primeFactors.card.

2) V2 Every odd weird number has at least two distinct prime factors.

kernel-checked, filed Tue Aug 25 2026 04:20:39 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All natural numbers; conditional on oddness and Mathlib's exact weird-number predicate.

1) V1 Does there exist a natural number that is both weird—abundant but not pseudoperfect—and odd?

open, filed Tue Aug 25 2026 04:17:57 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Mathlib's Nat.Weird is exactly abundance together with failure of pseudoperfectness. The affirmative existence proposition is the formal-conjectures interpretation of the yes/no question.

Scope. The odd-weird-number existence part of Erdős Problem 470; the separate primitive-weird infinitude question is not conflated with it.

E470:Erdős Problem #470 “Does an odd weird number exist?”

E470: “Does an odd weird number exist?”