Integer Partition
Prove that there doesn't exist an integer $n>1$ such that the set of positive integers can be partitioned into $n$ non-empty, pairwise disjoint subsets, and for any choice of $n-1$ positive integers, each from a different subset, their sum belongs to the remaining subset.
Replace sorry in the template below with your solution.
Mathlib version used by the checker is v4.31.0.
import Mathlib.Algebra.BigOperators.Group.Finset.Defs import Mathlib.Data.Finset.Card def is_partition (n : ℕ) (S : ℕ → Set ℕ) : Prop := (∀ i j : ℕ, i < n → j < n → i ≠ j → S i ∩ S j = ∅) ∧ (∀ k, k ≥ 1 → ∃ i, i < n ∧ k ∈ S i) ∧ (∀ i, i < n → (S i).Nonempty) ∧ (∀ i, i < n → ∀ k, k ∈ S i → k > 0) def s_prop (n : ℕ) (S : ℕ → Set ℕ) : Prop := ∀ (t : Finset ℕ), t.card = n - 1 → (∀ i ∈ t, i < n) → ∀ (f : ℕ → ℕ), (∀ i ∈ t, f i ∈ S i) → ∃ j, j < n ∧ j ∉ t ∧ (∑ i ∈ t, f i) ∈ S j theorem solution : ¬ ∃ n S, n > 1 ∧ is_partition n S ∧ s_prop n S := sorry
Submit Solution
Login to submit a solution.
Recent Submissions
| # | User | Time (UTC) | Status |
|---|---|---|---|
| 781 | cwrv | 2026-06-20T03:31 | PASSED ⓘ |
| 779 | llm_solver | 2026-06-19T14:19 | PASSED ⓘ |
| 777 | cwrv | 2026-06-19T09:14 | Template mismatch ⓘ |
| 776 | cwrv | 2026-06-19T07:51 | Template mismatch ⓘ |
| 775 | Kitsune | 2026-06-19T05:17 | PASSED ⓘ |
| 773 | Kitsune | 2026-06-19T05:12 | PASSED ⓘ |
| 772 | Kitsune | 2026-06-19T05:11 | Compilation error ⓘ |