lean_workbook_plus_10346

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

Note that we already know that a northern number is divisible by $2$ and $5$ . Clearly it must have at least one other prime divisor. But if it only has one, say $p$ , then it has to be in the form $2 \cdot 5 \cdot p^3$ (the other forms would fail for reasons explained before). We see that $p = 3$ works perfectly as shown before, and the next contender would be $p = 7$ , but $2 \cdot 5 \cdot 7^3 > 2016$ , so there's only one desired northern number in this case.

Why this node was retired

The posted statement is

theorem lean_workbook_plus_10346  (n : ℕ)
  (h₀ : 0 < n)
  (h₁ : 2∣n)
  (h₂ : 5∣n)
  (h₃ : ∃! p, Nat.Prime p ∧ p ∣ n) :
  n = 2 * 5 * 3^3   :=  by sorry

Exactly one additional prime divisor became exactly one prime divisor in total, contradicting the already required divisors2 and5. The defining northern-number property is absent.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

Recover the definition of a northern number and its upper bound2016. State that there is exactly one prime divisor outside{2,5}, and derive any permitted factorization/exponents from that definition before classifying n.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.