1. FormalConjectures
  2. ErdosProblems
  3. «470»
/- Copyright 2025 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

Erdős Problem 470

Reference: erdosproblems.com/470

namespace Erdos470

Primitive weird numbers are weird numbers such that no proper divisor of $n$ are weird.

def PrimitiveWeird (n : ℕ) := n.Weird ∧ ∀ d ∈ n.properDivisors, ¬d.Weird

The abundancy index is the sum of the divisors of $n$ divided by $n$.

def AbundancyIndex (n : ℕ) : ℚ := (∑ d ∈ n.divisors, d) / n

Are there any odd weird numbers?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_470.parts.i : answer(sorry) ↔ ∃ n : ℕ, n.Weird ∧ Odd n := ⊢ True ↔ ∃ n, n.Weird ∧ Odd n All goals completed! 🐙

Are there infinitely many primitive weird numbers?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_470.parts.ii : answer(sorry) ↔ Set.Infinite PrimitiveWeird := ⊢ True ↔ Set.Infinite PrimitiveWeird All goals completed! 🐙

Benkoski and Erdős BeEr74 proved that the set of weird numbers has positive density.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_470.variants.weird_pos_density : {n : ℕ | n.Weird}.HasPosDensity := ⊢ {n | n.Weird}.HasPosDensity All goals completed! 🐙

The smallest weird number is 70.

@[category textbook, AMS 11] theorem erdos_470.variants.smallest_weird_eq_70 : (∀ n < 70, ¬n.Weird) ∧ (70).Weird := ⊢ (∀ n < 70, ¬n.Weird) ∧ Nat.Weird 70 ⊢ ∀ n < 70, ¬n.Weird n:ℕhn:n < 70ha:n.Abundanthnp:¬n.Pseudoperfect⊢ False n:ℕhn:n < 70ha:n < ∑ i ∈ n.properDivisors, ihnp:¬n.Pseudoperfect⊢ False n:ℕhn:n < 70ha:n < ∑ i ∈ n.properDivisors, ihnp:¬n.Pseudoperfect⊢ n.Pseudoperfect -- For non-abundant `n`, `ha` is contradictory; for each abundant `n < 70`, exhibit an explicit -- subset of its proper divisors summing to `n` (so `n` is pseudoperfect, hence not weird). n:ℕhn:0 < 70ha:0 < ∑ i ∈ Nat.properDivisors 0, ihnp:¬Nat.Pseudoperfect 0⊢ Nat.Pseudoperfect 0n:ℕhn:1 < 70ha:1 < ∑ i ∈ Nat.properDivisors 1, ihnp:¬Nat.Pseudoperfect 1⊢ Nat.Pseudoperfect 1n:ℕhn:2 < 70ha:2 < ∑ i ∈ Nat.properDivisors 2, ihnp:¬Nat.Pseudoperfect 2⊢ Nat.Pseudoperfect 2n:ℕhn:3 < 70ha:3 < ∑ i ∈ Nat.properDivisors 3, ihnp:¬Nat.Pseudoperfect 3⊢ Nat.Pseudoperfect 3n:ℕhn:4 < 70ha:4 < ∑ i ∈ Nat.properDivisors 4, ihnp:¬Nat.Pseudoperfect 4⊢ Nat.Pseudoperfect 4n:ℕhn:5 < 70ha:5 < ∑ i ∈ Nat.properDivisors 5, ihnp:¬Nat.Pseudoperfect 5⊢ Nat.Pseudoperfect 5n:ℕhn:6 < 70ha:6 < ∑ i ∈ Nat.properDivisors 6, ihnp:¬Nat.Pseudoperfect 6⊢ Nat.Pseudoperfect 6n:ℕhn:7 < 70ha:7 < ∑ i ∈ Nat.properDivisors 7, ihnp:¬Nat.Pseudoperfect 7⊢ Nat.Pseudoperfect 7n:ℕhn:8 < 70ha:8 < ∑ i ∈ Nat.properDivisors 8, ihnp:¬Nat.Pseudoperfect 8⊢ Nat.Pseudoperfect 8n:ℕhn:9 < 70ha:9 < ∑ i ∈ Nat.properDivisors 9, ihnp:¬Nat.Pseudoperfect 9⊢ Nat.Pseudoperfect 9n:ℕhn:10 < 70ha:10 < ∑ i ∈ Nat.properDivisors 10, ihnp:¬Nat.Pseudoperfect 10⊢ Nat.Pseudoperfect 10n:ℕhn:11 < 70ha:11 < ∑ i ∈ Nat.properDivisors 11, ihnp:¬Nat.Pseudoperfect 11⊢ Nat.Pseudoperfect 11n:ℕhn:12 < 70ha:12 < ∑ i ∈ Nat.properDivisors 12, ihnp:¬Nat.Pseudoperfect 12⊢ Nat.Pseudoperfect 12n:ℕhn:13 < 70ha:13 < ∑ i ∈ Nat.properDivisors 13, ihnp:¬Nat.Pseudoperfect 13⊢ Nat.Pseudoperfect 13n:ℕhn:14 < 70ha:14 < ∑ i ∈ Nat.properDivisors 14, ihnp:¬Nat.Pseudoperfect 14⊢ Nat.Pseudoperfect 14n:ℕhn:15 < 70ha:15 < ∑ i ∈ Nat.properDivisors 15, ihnp:¬Nat.Pseudoperfect 15⊢ Nat.Pseudoperfect 15n:ℕhn:16 < 70ha:16 < ∑ i ∈ Nat.properDivisors 16, ihnp:¬Nat.Pseudoperfect 16⊢ Nat.Pseudoperfect 16n:ℕhn:17 < 70ha:17 < ∑ i ∈ Nat.properDivisors 17, ihnp:¬Nat.Pseudoperfect 17⊢ Nat.Pseudoperfect 17n:ℕhn:18 < 70ha:18 < ∑ i ∈ Nat.properDivisors 18, ihnp:¬Nat.Pseudoperfect 18⊢ Nat.Pseudoperfect 18n:ℕhn:19 < 70ha:19 < ∑ i ∈ Nat.properDivisors 19, ihnp:¬Nat.Pseudoperfect 19⊢ Nat.Pseudoperfect 19n:ℕhn:20 < 70ha:20 < ∑ i ∈ Nat.properDivisors 20, ihnp:¬Nat.Pseudoperfect 20⊢ Nat.Pseudoperfect 20n:ℕhn:21 < 70ha:21 < ∑ i ∈ Nat.properDivisors 21, ihnp:¬Nat.Pseudoperfect 21⊢ Nat.Pseudoperfect 21n:ℕhn:22 < 70ha:22 < ∑ i ∈ Nat.properDivisors 22, ihnp:¬Nat.Pseudoperfect 22⊢ Nat.Pseudoperfect 22n:ℕhn:23 < 70ha:23 < ∑ i ∈ Nat.properDivisors 23, ihnp:¬Nat.Pseudoperfect 23⊢ Nat.Pseudoperfect 23n:ℕhn:24 < 70ha:24 < ∑ i ∈ Nat.properDivisors 24, ihnp:¬Nat.Pseudoperfect 24⊢ Nat.Pseudoperfect 24n:ℕhn:25 < 70ha:25 < ∑ i ∈ Nat.properDivisors 25, ihnp:¬Nat.Pseudoperfect 25⊢ Nat.Pseudoperfect 25n:ℕhn:26 < 70ha:26 < ∑ i ∈ Nat.properDivisors 26, ihnp:¬Nat.Pseudoperfect 26⊢ Nat.Pseudoperfect 26n:ℕhn:27 < 70ha:27 < ∑ i ∈ Nat.properDivisors 27, ihnp:¬Nat.Pseudoperfect 27⊢ Nat.Pseudoperfect 27n:ℕhn:28 < 70ha:28 < ∑ i ∈ Nat.properDivisors 28, ihnp:¬Nat.Pseudoperfect 28⊢ Nat.Pseudoperfect 28n:ℕhn:29 < 70ha:29 < ∑ i ∈ Nat.properDivisors 29, ihnp:¬Nat.Pseudoperfect 29⊢ Nat.Pseudoperfect 29n:ℕhn:30 < 70ha:30 < ∑ i ∈ Nat.properDivisors 30, ihnp:¬Nat.Pseudoperfect 30⊢ Nat.Pseudoperfect 30n:ℕhn:31 < 70ha:31 < ∑ i ∈ Nat.properDivisors 31, ihnp:¬Nat.Pseudoperfect 31⊢ Nat.Pseudoperfect 31n:ℕhn:32 < 70ha:32 < ∑ i ∈ Nat.properDivisors 32, ihnp:¬Nat.Pseudoperfect 32⊢ Nat.Pseudoperfect 32n:ℕhn:33 < 70ha:33 < ∑ i ∈ Nat.properDivisors 33, ihnp:¬Nat.Pseudoperfect 33⊢ Nat.Pseudoperfect 33n:ℕhn:34 < 70ha:34 < ∑ i ∈ Nat.properDivisors 34, ihnp:¬Nat.Pseudoperfect 34⊢ Nat.Pseudoperfect 34n:ℕhn:35 < 70ha:35 < ∑ i ∈ Nat.properDivisors 35, ihnp:¬Nat.Pseudoperfect 35⊢ Nat.Pseudoperfect 35n:ℕhn:36 < 70ha:36 < ∑ i ∈ Nat.properDivisors 36, ihnp:¬Nat.Pseudoperfect 36⊢ Nat.Pseudoperfect 36n:ℕhn:37 < 70ha:37 < ∑ i ∈ Nat.properDivisors 37, ihnp:¬Nat.Pseudoperfect 37⊢ Nat.Pseudoperfect 37n:ℕhn:38 < 70ha:38 < ∑ i ∈ Nat.properDivisors 38, ihnp:¬Nat.Pseudoperfect 38⊢ Nat.Pseudoperfect 38n:ℕhn:39 < 70ha:39 < ∑ i ∈ Nat.properDivisors 39, ihnp:¬Nat.Pseudoperfect 39⊢ Nat.Pseudoperfect 39n:ℕhn:40 < 70ha:40 < ∑ i ∈ Nat.properDivisors 40, ihnp:¬Nat.Pseudoperfect 40⊢ Nat.Pseudoperfect 40n:ℕhn:41 < 70ha:41 < ∑ i ∈ Nat.properDivisors 41, ihnp:¬Nat.Pseudoperfect 41⊢ Nat.Pseudoperfect 41n:ℕhn:42 < 70ha:42 < ∑ i ∈ Nat.properDivisors 42, ihnp:¬Nat.Pseudoperfect 42⊢ Nat.Pseudoperfect 42n:ℕhn:43 < 70ha:43 < ∑ i ∈ Nat.properDivisors 43, ihnp:¬Nat.Pseudoperfect 43⊢ Nat.Pseudoperfect 43n:ℕhn:44 < 70ha:44 < ∑ i ∈ Nat.properDivisors 44, ihnp:¬Nat.Pseudoperfect 44⊢ Nat.Pseudoperfect 44n:ℕhn:45 < 70ha:45 < ∑ i ∈ Nat.properDivisors 45, ihnp:¬Nat.Pseudoperfect 45⊢ Nat.Pseudoperfect 45n:ℕhn:46 < 70ha:46 < ∑ i ∈ Nat.properDivisors 46, ihnp:¬Nat.Pseudoperfect 46⊢ Nat.Pseudoperfect 46n:ℕhn:47 < 70ha:47 < ∑ i ∈ Nat.properDivisors 47, ihnp:¬Nat.Pseudoperfect 47⊢ Nat.Pseudoperfect 47n:ℕhn:48 < 70ha:48 < ∑ i ∈ Nat.properDivisors 48, ihnp:¬Nat.Pseudoperfect 48⊢ Nat.Pseudoperfect 48n:ℕhn:49 < 70ha:49 < ∑ i ∈ Nat.properDivisors 49, ihnp:¬Nat.Pseudoperfect 49⊢ Nat.Pseudoperfect 49n:ℕhn:50 < 70ha:50 < ∑ i ∈ Nat.properDivisors 50, ihnp:¬Nat.Pseudoperfect 50⊢ Nat.Pseudoperfect 50n:ℕhn:51 < 70ha:51 < ∑ i ∈ Nat.properDivisors 51, ihnp:¬Nat.Pseudoperfect 51⊢ Nat.Pseudoperfect 51n:ℕhn:52 < 70ha:52 < ∑ i ∈ Nat.properDivisors 52, ihnp:¬Nat.Pseudoperfect 52⊢ Nat.Pseudoperfect 52n:ℕhn:53 < 70ha:53 < ∑ i ∈ Nat.properDivisors 53, ihnp:¬Nat.Pseudoperfect 53⊢ Nat.Pseudoperfect 53n:ℕhn:54 < 70ha:54 < ∑ i ∈ Nat.properDivisors 54, ihnp:¬Nat.Pseudoperfect 54⊢ Nat.Pseudoperfect 54n:ℕhn:55 < 70ha:55 < ∑ i ∈ Nat.properDivisors 55, ihnp:¬Nat.Pseudoperfect 55⊢ Nat.Pseudoperfect 55n:ℕhn:56 < 70ha:56 < ∑ i ∈ Nat.properDivisors 56, ihnp:¬Nat.Pseudoperfect 56⊢ Nat.Pseudoperfect 56n:ℕhn:57 < 70ha:57 < ∑ i ∈ Nat.properDivisors 57, ihnp:¬Nat.Pseudoperfect 57⊢ Nat.Pseudoperfect 57n:ℕhn:58 < 70ha:58 < ∑ i ∈ Nat.properDivisors 58, ihnp:¬Nat.Pseudoperfect 58⊢ Nat.Pseudoperfect 58n:ℕhn:59 < 70ha:59 < ∑ i ∈ Nat.properDivisors 59, ihnp:¬Nat.Pseudoperfect 59⊢ Nat.Pseudoperfect 59n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ Nat.Pseudoperfect 60n:ℕhn:61 < 70ha:61 < ∑ i ∈ Nat.properDivisors 61, ihnp:¬Nat.Pseudoperfect 61⊢ Nat.Pseudoperfect 61n:ℕhn:62 < 70ha:62 < ∑ i ∈ Nat.properDivisors 62, ihnp:¬Nat.Pseudoperfect 62⊢ Nat.Pseudoperfect 62n:ℕhn:63 < 70ha:63 < ∑ i ∈ Nat.properDivisors 63, ihnp:¬Nat.Pseudoperfect 63⊢ Nat.Pseudoperfect 63n:ℕhn:64 < 70ha:64 < ∑ i ∈ Nat.properDivisors 64, ihnp:¬Nat.Pseudoperfect 64⊢ Nat.Pseudoperfect 64n:ℕhn:65 < 70ha:65 < ∑ i ∈ Nat.properDivisors 65, ihnp:¬Nat.Pseudoperfect 65⊢ Nat.Pseudoperfect 65n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ Nat.Pseudoperfect 66n:ℕhn:67 < 70ha:67 < ∑ i ∈ Nat.properDivisors 67, ihnp:¬Nat.Pseudoperfect 67⊢ Nat.Pseudoperfect 67n:ℕhn:68 < 70ha:68 < ∑ i ∈ Nat.properDivisors 68, ihnp:¬Nat.Pseudoperfect 68⊢ Nat.Pseudoperfect 68n:ℕhn:69 < 70ha:69 < ∑ i ∈ Nat.properDivisors 69, ihnp:¬Nat.Pseudoperfect 69⊢ Nat.Pseudoperfect 69 n:ℕhn:0 < 70ha:0 < ∑ i ∈ Nat.properDivisors 0, ihnp:¬Nat.Pseudoperfect 0⊢ Nat.Pseudoperfect 0n:ℕhn:1 < 70ha:1 < ∑ i ∈ Nat.properDivisors 1, ihnp:¬Nat.Pseudoperfect 1⊢ Nat.Pseudoperfect 1n:ℕhn:2 < 70ha:2 < ∑ i ∈ Nat.properDivisors 2, ihnp:¬Nat.Pseudoperfect 2⊢ Nat.Pseudoperfect 2n:ℕhn:3 < 70ha:3 < ∑ i ∈ Nat.properDivisors 3, ihnp:¬Nat.Pseudoperfect 3⊢ Nat.Pseudoperfect 3n:ℕhn:4 < 70ha:4 < ∑ i ∈ Nat.properDivisors 4, ihnp:¬Nat.Pseudoperfect 4⊢ Nat.Pseudoperfect 4n:ℕhn:5 < 70ha:5 < ∑ i ∈ Nat.properDivisors 5, ihnp:¬Nat.Pseudoperfect 5⊢ Nat.Pseudoperfect 5n:ℕhn:6 < 70ha:6 < ∑ i ∈ Nat.properDivisors 6, ihnp:¬Nat.Pseudoperfect 6⊢ Nat.Pseudoperfect 6n:ℕhn:7 < 70ha:7 < ∑ i ∈ Nat.properDivisors 7, ihnp:¬Nat.Pseudoperfect 7⊢ Nat.Pseudoperfect 7n:ℕhn:8 < 70ha:8 < ∑ i ∈ Nat.properDivisors 8, ihnp:¬Nat.Pseudoperfect 8⊢ Nat.Pseudoperfect 8n:ℕhn:9 < 70ha:9 < ∑ i ∈ Nat.properDivisors 9, ihnp:¬Nat.Pseudoperfect 9⊢ Nat.Pseudoperfect 9n:ℕhn:10 < 70ha:10 < ∑ i ∈ Nat.properDivisors 10, ihnp:¬Nat.Pseudoperfect 10⊢ Nat.Pseudoperfect 10n:ℕhn:11 < 70ha:11 < ∑ i ∈ Nat.properDivisors 11, ihnp:¬Nat.Pseudoperfect 11⊢ Nat.Pseudoperfect 11n:ℕhn:12 < 70ha:12 < ∑ i ∈ Nat.properDivisors 12, ihnp:¬Nat.Pseudoperfect 12⊢ Nat.Pseudoperfect 12n:ℕhn:13 < 70ha:13 < ∑ i ∈ Nat.properDivisors 13, ihnp:¬Nat.Pseudoperfect 13⊢ Nat.Pseudoperfect 13n:ℕhn:14 < 70ha:14 < ∑ i ∈ Nat.properDivisors 14, ihnp:¬Nat.Pseudoperfect 14⊢ Nat.Pseudoperfect 14n:ℕhn:15 < 70ha:15 < ∑ i ∈ Nat.properDivisors 15, ihnp:¬Nat.Pseudoperfect 15⊢ Nat.Pseudoperfect 15n:ℕhn:16 < 70ha:16 < ∑ i ∈ Nat.properDivisors 16, ihnp:¬Nat.Pseudoperfect 16⊢ Nat.Pseudoperfect 16n:ℕhn:17 < 70ha:17 < ∑ i ∈ Nat.properDivisors 17, ihnp:¬Nat.Pseudoperfect 17⊢ Nat.Pseudoperfect 17n:ℕhn:18 < 70ha:18 < ∑ i ∈ Nat.properDivisors 18, ihnp:¬Nat.Pseudoperfect 18⊢ Nat.Pseudoperfect 18n:ℕhn:19 < 70ha:19 < ∑ i ∈ Nat.properDivisors 19, ihnp:¬Nat.Pseudoperfect 19⊢ Nat.Pseudoperfect 19n:ℕhn:20 < 70ha:20 < ∑ i ∈ Nat.properDivisors 20, ihnp:¬Nat.Pseudoperfect 20⊢ Nat.Pseudoperfect 20n:ℕhn:21 < 70ha:21 < ∑ i ∈ Nat.properDivisors 21, ihnp:¬Nat.Pseudoperfect 21⊢ Nat.Pseudoperfect 21n:ℕhn:22 < 70ha:22 < ∑ i ∈ Nat.properDivisors 22, ihnp:¬Nat.Pseudoperfect 22⊢ Nat.Pseudoperfect 22n:ℕhn:23 < 70ha:23 < ∑ i ∈ Nat.properDivisors 23, ihnp:¬Nat.Pseudoperfect 23⊢ Nat.Pseudoperfect 23n:ℕhn:24 < 70ha:24 < ∑ i ∈ Nat.properDivisors 24, ihnp:¬Nat.Pseudoperfect 24⊢ Nat.Pseudoperfect 24n:ℕhn:25 < 70ha:25 < ∑ i ∈ Nat.properDivisors 25, ihnp:¬Nat.Pseudoperfect 25⊢ Nat.Pseudoperfect 25n:ℕhn:26 < 70ha:26 < ∑ i ∈ Nat.properDivisors 26, ihnp:¬Nat.Pseudoperfect 26⊢ Nat.Pseudoperfect 26n:ℕhn:27 < 70ha:27 < ∑ i ∈ Nat.properDivisors 27, ihnp:¬Nat.Pseudoperfect 27⊢ Nat.Pseudoperfect 27n:ℕhn:28 < 70ha:28 < ∑ i ∈ Nat.properDivisors 28, ihnp:¬Nat.Pseudoperfect 28⊢ Nat.Pseudoperfect 28n:ℕhn:29 < 70ha:29 < ∑ i ∈ Nat.properDivisors 29, ihnp:¬Nat.Pseudoperfect 29⊢ Nat.Pseudoperfect 29n:ℕhn:30 < 70ha:30 < ∑ i ∈ Nat.properDivisors 30, ihnp:¬Nat.Pseudoperfect 30⊢ Nat.Pseudoperfect 30n:ℕhn:31 < 70ha:31 < ∑ i ∈ Nat.properDivisors 31, ihnp:¬Nat.Pseudoperfect 31⊢ Nat.Pseudoperfect 31n:ℕhn:32 < 70ha:32 < ∑ i ∈ Nat.properDivisors 32, ihnp:¬Nat.Pseudoperfect 32⊢ Nat.Pseudoperfect 32n:ℕhn:33 < 70ha:33 < ∑ i ∈ Nat.properDivisors 33, ihnp:¬Nat.Pseudoperfect 33⊢ Nat.Pseudoperfect 33n:ℕhn:34 < 70ha:34 < ∑ i ∈ Nat.properDivisors 34, ihnp:¬Nat.Pseudoperfect 34⊢ Nat.Pseudoperfect 34n:ℕhn:35 < 70ha:35 < ∑ i ∈ Nat.properDivisors 35, ihnp:¬Nat.Pseudoperfect 35⊢ Nat.Pseudoperfect 35n:ℕhn:36 < 70ha:36 < ∑ i ∈ Nat.properDivisors 36, ihnp:¬Nat.Pseudoperfect 36⊢ Nat.Pseudoperfect 36n:ℕhn:37 < 70ha:37 < ∑ i ∈ Nat.properDivisors 37, ihnp:¬Nat.Pseudoperfect 37⊢ Nat.Pseudoperfect 37n:ℕhn:38 < 70ha:38 < ∑ i ∈ Nat.properDivisors 38, ihnp:¬Nat.Pseudoperfect 38⊢ Nat.Pseudoperfect 38n:ℕhn:39 < 70ha:39 < ∑ i ∈ Nat.properDivisors 39, ihnp:¬Nat.Pseudoperfect 39⊢ Nat.Pseudoperfect 39n:ℕhn:40 < 70ha:40 < ∑ i ∈ Nat.properDivisors 40, ihnp:¬Nat.Pseudoperfect 40⊢ Nat.Pseudoperfect 40n:ℕhn:41 < 70ha:41 < ∑ i ∈ Nat.properDivisors 41, ihnp:¬Nat.Pseudoperfect 41⊢ Nat.Pseudoperfect 41n:ℕhn:42 < 70ha:42 < ∑ i ∈ Nat.properDivisors 42, ihnp:¬Nat.Pseudoperfect 42⊢ Nat.Pseudoperfect 42n:ℕhn:43 < 70ha:43 < ∑ i ∈ Nat.properDivisors 43, ihnp:¬Nat.Pseudoperfect 43⊢ Nat.Pseudoperfect 43n:ℕhn:44 < 70ha:44 < ∑ i ∈ Nat.properDivisors 44, ihnp:¬Nat.Pseudoperfect 44⊢ Nat.Pseudoperfect 44n:ℕhn:45 < 70ha:45 < ∑ i ∈ Nat.properDivisors 45, ihnp:¬Nat.Pseudoperfect 45⊢ Nat.Pseudoperfect 45n:ℕhn:46 < 70ha:46 < ∑ i ∈ Nat.properDivisors 46, ihnp:¬Nat.Pseudoperfect 46⊢ Nat.Pseudoperfect 46n:ℕhn:47 < 70ha:47 < ∑ i ∈ Nat.properDivisors 47, ihnp:¬Nat.Pseudoperfect 47⊢ Nat.Pseudoperfect 47n:ℕhn:48 < 70ha:48 < ∑ i ∈ Nat.properDivisors 48, ihnp:¬Nat.Pseudoperfect 48⊢ Nat.Pseudoperfect 48n:ℕhn:49 < 70ha:49 < ∑ i ∈ Nat.properDivisors 49, ihnp:¬Nat.Pseudoperfect 49⊢ Nat.Pseudoperfect 49n:ℕhn:50 < 70ha:50 < ∑ i ∈ Nat.properDivisors 50, ihnp:¬Nat.Pseudoperfect 50⊢ Nat.Pseudoperfect 50n:ℕhn:51 < 70ha:51 < ∑ i ∈ Nat.properDivisors 51, ihnp:¬Nat.Pseudoperfect 51⊢ Nat.Pseudoperfect 51n:ℕhn:52 < 70ha:52 < ∑ i ∈ Nat.properDivisors 52, ihnp:¬Nat.Pseudoperfect 52⊢ Nat.Pseudoperfect 52n:ℕhn:53 < 70ha:53 < ∑ i ∈ Nat.properDivisors 53, ihnp:¬Nat.Pseudoperfect 53⊢ Nat.Pseudoperfect 53n:ℕhn:54 < 70ha:54 < ∑ i ∈ Nat.properDivisors 54, ihnp:¬Nat.Pseudoperfect 54⊢ Nat.Pseudoperfect 54n:ℕhn:55 < 70ha:55 < ∑ i ∈ Nat.properDivisors 55, ihnp:¬Nat.Pseudoperfect 55⊢ Nat.Pseudoperfect 55n:ℕhn:56 < 70ha:56 < ∑ i ∈ Nat.properDivisors 56, ihnp:¬Nat.Pseudoperfect 56⊢ Nat.Pseudoperfect 56n:ℕhn:57 < 70ha:57 < ∑ i ∈ Nat.properDivisors 57, ihnp:¬Nat.Pseudoperfect 57⊢ Nat.Pseudoperfect 57n:ℕhn:58 < 70ha:58 < ∑ i ∈ Nat.properDivisors 58, ihnp:¬Nat.Pseudoperfect 58⊢ Nat.Pseudoperfect 58n:ℕhn:59 < 70ha:59 < ∑ i ∈ Nat.properDivisors 59, ihnp:¬Nat.Pseudoperfect 59⊢ Nat.Pseudoperfect 59n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ Nat.Pseudoperfect 60n:ℕhn:61 < 70ha:61 < ∑ i ∈ Nat.properDivisors 61, ihnp:¬Nat.Pseudoperfect 61⊢ Nat.Pseudoperfect 61n:ℕhn:62 < 70ha:62 < ∑ i ∈ Nat.properDivisors 62, ihnp:¬Nat.Pseudoperfect 62⊢ Nat.Pseudoperfect 62n:ℕhn:63 < 70ha:63 < ∑ i ∈ Nat.properDivisors 63, ihnp:¬Nat.Pseudoperfect 63⊢ Nat.Pseudoperfect 63n:ℕhn:64 < 70ha:64 < ∑ i ∈ Nat.properDivisors 64, ihnp:¬Nat.Pseudoperfect 64⊢ Nat.Pseudoperfect 64n:ℕhn:65 < 70ha:65 < ∑ i ∈ Nat.properDivisors 65, ihnp:¬Nat.Pseudoperfect 65⊢ Nat.Pseudoperfect 65n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ Nat.Pseudoperfect 66n:ℕhn:67 < 70ha:67 < ∑ i ∈ Nat.properDivisors 67, ihnp:¬Nat.Pseudoperfect 67⊢ Nat.Pseudoperfect 67n:ℕhn:68 < 70ha:68 < ∑ i ∈ Nat.properDivisors 68, ihnp:¬Nat.Pseudoperfect 68⊢ Nat.Pseudoperfect 68n:ℕhn:69 < 70ha:69 < ∑ i ∈ Nat.properDivisors 69, ihnp:¬Nat.Pseudoperfect 69⊢ Nat.Pseudoperfect 69 first | exact absurd ha (n:ℕhn:69 < 70ha:69 < ∑ i ∈ Nat.properDivisors 69, ihnp:¬Nat.Pseudoperfect 69⊢ ¬69 < ∑ i ∈ Nat.properDivisors 69, i All goals completed! 🐙) | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({2, 4, 6} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {2, 4, 6} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {2, 4, 6} ⊆ Nat.properDivisors 66, n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ ∑ i ∈ {2, 4, 6}, i = 60 n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ ∑ i ∈ {2, 4, 6}, i = 60⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({3, 6, 9} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {3, 6, 9} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {3, 6, 9} ⊆ Nat.properDivisors 66, n:ℕhn:54 < 70ha:54 < ∑ i ∈ Nat.properDivisors 54, ihnp:¬Nat.Pseudoperfect 54⊢ ∑ i ∈ {3, 6, 9}, i = 54 n:ℕhn:54 < 70ha:54 < ∑ i ∈ Nat.properDivisors 54, ihnp:¬Nat.Pseudoperfect 54⊢ ∑ i ∈ {3, 6, 9}, i = 54⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({1, 4, 5, 10} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {1, 4, 5, 10} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {1, 4, 5, 10} ⊆ Nat.properDivisors 66, n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ ∑ i ∈ {1, 4, 5, 10}, i = 60 n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ ∑ i ∈ {1, 4, 5, 10}, i = 60⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({4, 8, 12} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {4, 8, 12} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {4, 8, 12} ⊆ Nat.properDivisors 66, n:ℕhn:48 < 70ha:48 < ∑ i ∈ Nat.properDivisors 48, ihnp:¬Nat.Pseudoperfect 48⊢ ∑ i ∈ {4, 8, 12}, i = 48 n:ℕhn:48 < 70ha:48 < ∑ i ∈ Nat.properDivisors 48, ihnp:¬Nat.Pseudoperfect 48⊢ ∑ i ∈ {4, 8, 12}, i = 48⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({5, 10, 15} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {5, 10, 15} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {5, 10, 15} ⊆ Nat.properDivisors 66, n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ ∑ i ∈ {5, 10, 15}, i = 60 n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ ∑ i ∈ {5, 10, 15}, i = 60⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({6, 12, 18} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {6, 12, 18} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {6, 12, 18} ⊆ Nat.properDivisors 66, n:ℕhn:36 < 70ha:36 < ∑ i ∈ Nat.properDivisors 36, ihnp:¬Nat.Pseudoperfect 36⊢ ∑ i ∈ {6, 12, 18}, i = 36 All goals completed! 🐙⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({2, 8, 10, 20} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {2, 8, 10, 20} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {2, 8, 10, 20} ⊆ Nat.properDivisors 66, n:ℕhn:40 < 70ha:40 < ∑ i ∈ Nat.properDivisors 40, ihnp:¬Nat.Pseudoperfect 40⊢ ∑ i ∈ {2, 8, 10, 20}, i = 40 All goals completed! 🐙⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({7, 14, 21} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {7, 14, 21} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {7, 14, 21} ⊆ Nat.properDivisors 66, n:ℕhn:42 < 70ha:42 < ∑ i ∈ Nat.properDivisors 42, ihnp:¬Nat.Pseudoperfect 42⊢ ∑ i ∈ {7, 14, 21}, i = 42 All goals completed! 🐙⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({8, 16, 24} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {8, 16, 24} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {8, 16, 24} ⊆ Nat.properDivisors 66, n:ℕhn:48 < 70ha:48 < ∑ i ∈ Nat.properDivisors 48, ihnp:¬Nat.Pseudoperfect 48⊢ ∑ i ∈ {8, 16, 24}, i = 48 All goals completed! 🐙⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({9, 18, 27} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {9, 18, 27} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {9, 18, 27} ⊆ Nat.properDivisors 66, n:ℕhn:54 < 70ha:54 < ∑ i ∈ Nat.properDivisors 54, ihnp:¬Nat.Pseudoperfect 54⊢ ∑ i ∈ {9, 18, 27}, i = 54 All goals completed! 🐙⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({2, 4, 8, 14, 28} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {2, 4, 8, 14, 28} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {2, 4, 8, 14, 28} ⊆ Nat.properDivisors 66, n:ℕhn:56 < 70ha:56 < ∑ i ∈ Nat.properDivisors 56, ihnp:¬Nat.Pseudoperfect 56⊢ ∑ i ∈ {2, 4, 8, 14, 28}, i = 56 All goals completed! 🐙⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({10, 20, 30} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {10, 20, 30} ⊆ Nat.properDivisors 66 n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {10, 20, 30} ⊆ Nat.properDivisors 66, n:ℕhn:60 < 70ha:60 < ∑ i ∈ Nat.properDivisors 60, ihnp:¬Nat.Pseudoperfect 60⊢ ∑ i ∈ {10, 20, 30}, i = 60 All goals completed! 🐙⟩ | exact ⟨n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ 0 < 66 All goals completed! 🐙, ({11, 22, 33} : Finset ℕ), n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ {11, 22, 33} ⊆ Nat.properDivisors 66 All goals completed! 🐙, n:ℕhn:66 < 70ha:66 < ∑ i ∈ Nat.properDivisors 66, ihnp:¬Nat.Pseudoperfect 66⊢ ∑ i ∈ {11, 22, 33}, i = 66 All goals completed! 🐙⟩

Melfi Me15 has proved that there are infinitely many primitive weird numbers, conditional on the fact that $p_{n+1} - p_n < \frac{1}{10} \sqrt{p_n}$ for all large $n$, which in turn would follow from well-known conjectures concerning prime gaps.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_470.variants.prime_gap_imp_inf_prim_weird : (∀ᶠ n in Filter.atTop, primeGap n < √ (n.nth Nat.Prime) / 10) → Set.Infinite PrimitiveWeird := ⊢ (∀ᶠ (n : ℕ) in Filter.atTop, ↑(primeGap n) < √↑(Nat.nth Nat.Prime n) / 10) → Set.Infinite PrimitiveWeird All goals completed! 🐙

Fang Fa22 has shown there are no odd weird numbers below $10^{21}$.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_470.variants.odd_weird_10_pow_21 : ∀ n < 10 ^ 21, Odd n → ¬n.Weird := ⊢ ∀ n < 10 ^ 21, Odd n → ¬n.Weird All goals completed! 🐙

Liddy and Riedl LiRi18 have shown that an odd weird number must have at least 6 prime divisors.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_470.variants.odd_weird_prime_div : ∀ n : ℕ, Odd n → n.Weird → 6 ≤ {m | m ∈ n.divisors ∧ m.Prime}.ncard := ⊢ ∀ (n : ℕ), Odd n → n.Weird → 6 ≤ {m | m ∈ n.divisors ∧ Nat.Prime m}.ncard All goals completed! 🐙

If there are no odd weird numbers then every weird number has abundancy index < 4.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_470.variants.abundancy_index : (∀ n : ℕ, n.Weird → ¬Odd n) → ∀ n, n.Weird → AbundancyIndex n < 4 := ⊢ (∀ (n : ℕ), n.Weird → ¬Odd n) → ∀ (n : ℕ), n.Weird → AbundancyIndex n < 4 All goals completed! 🐙 end Erdos470