In FormalConjectures/ErdosProblems/470.lean, the textbook variant
@[category textbook, AMS 11]
theorem erdos_470.variants.smallest_weird_eq_70 :
(∀ n < 70, ¬ n.Weird) ∧ (70).Weirdis the standard fact that $70$ is the smallest weird number (abundant but not pseudoperfect).
Nat.weird_seventy : Weird 70 already exists in Mathlib (Mathlib.NumberTheory.FactorisationProperties). The remaining direction — no $n < 70$ is weird — is a 70-case finite check.
Nat.Weird itself has no Decidable instance in Mathlib because Nat.Pseudoperfect uses an existential over arbitrary Finset ℕ (∃ s ⊆ properDivisors n, ∑ i ∈ s, i = n). After rewriting the bounded existential into one over (properDivisors n).powerset, the predicate is finite-decidable, and native_decide finishes the proof in well under a second per case.
I have a working proof (≈4 line tactic block + 3 local Decidable instances) and will open a PR.
In
FormalConjectures/ErdosProblems/470.lean, the textbook variantis the standard fact that$70$ is the smallest weird number (abundant but not pseudoperfect).
Nat.weird_seventy : Weird 70already exists in Mathlib (Mathlib.NumberTheory.FactorisationProperties). The remaining direction — noNat.Weirditself has noDecidableinstance in Mathlib becauseNat.Pseudoperfectuses an existential over arbitraryFinset ℕ(∃ s ⊆ properDivisors n, ∑ i ∈ s, i = n). After rewriting the bounded existential into one over(properDivisors n).powerset, the predicate is finite-decidable, andnative_decidefinishes the proof in well under a second per case.I have a working proof (≈4 line tactic block + 3 local
Decidableinstances) and will open a PR.