lean_workbook_plus_82333

⚠️ Retired — specification defect

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

Suppose that such an $S$ exists. Then there exists a natural number $n \not\in S$ . Since only $n$ elements of $S$ are coprime to $n$ it follows that infinitely many primes are not in $S$ . Let $p, q$ be distinct primes not in $S$ . Then there are only finitely many natural numbers $i$ such that $p^i$ is in $S$ , for otherwise we will violate the given condition for $q \not\in S$ . Let $i \ge 2$ be such that $p^i \not\in S$ . There are $p^i$ elements in $S$ that are coprime to $p^i$ , and these are coprime to $p$ as well. This is a contradiction since $p^i > p$ . Therefore such a set does not exist.

Why this node was retired

The posted statement is

theorem lean_workbook_plus_82333 : ¬∃ S : Set ℕ, ∀ n : ℕ, n ∈ S ∨ (∀ m : ℕ, m ∈ S → Nat.Coprime n m)   :=  by sorry

The source’s properness and exact coprime counts are missing; the complete original assumptions on S should be checked.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Restore the prescribed counting condition: for every n outside a proper subset S, the set of members of S coprime to n has exactly n elements. Replace the universal coprimality disjunction by that cardinality condition.

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.