feat: balanceable k-bounded partitions

LeanEval/Combinatorics/BalanceableBoundedPartitions.lean

@@ -0,0 +1,37 @@
+import Mathlib.Combinatorics.Enumerative.Partition.Basic
+import Mathlib.Algebra.GCDMonoid.Finset
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Combinatorics
+
+/--
+A partition is `k`-bounded if all of its members are at most `k`.
+
+For example, `12 = 3 + 2 + 2 + 2 + 2 + 1` is a `3`-bounded partition
+of `12`.
+-/
+def Bounded {n : ℕ} (k : ℕ) (p : n.Partition) : Prop :=
+  ∀ i ∈ p.parts, i ≤ k
+
+/--
+A partition is balanceable if it can be decoposed into two multisets of
+the same size.
+
+For example, `12 = (3 + 2 + 1) + (2 + 2 + 2)` is a balanceable partition
+of `12`.
+-/
+def Balanceable {n : ℕ} (p : n.Partition) : Prop :=
+  ∃ s₁ s₂, s₁ + s₂ = p.parts ∧ s₁.sum = s₂.sum
+
+/--
+For any `k`, the smallest `n` such that any `k`-bounded partition of `n` is
+also balanceable is given by `2 * lcm(1, ..., k)`.
+-/
+@[eval_problem]
+theorem minimal_balanceable_of_bounded (k : ℕ) (hk : 0 < k) :
+    Minimal (fun n => 0 < n ∧ ∀ p : n.Partition, Bounded k p → Balanceable p) (2 * (Finset.Icc 1 k).lcm id) := by
+  sorry
+
+end Combinatorics
+end LeanEval

manifests/problems.toml

@@ -645,3 +645,12 @@ module = "LeanEval.NumberTheory.NeukirchUchida"
 holes = ["neukirch_uchida"]
 submitter = "Junyan Xu"
 source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1."
+
+[[problem]]
+id = "balanceable_bounded_partitions"
+title = "Balanceable k-bounded partitions"
+test = false
+module = "LeanEval.Combinatorics.BalanceableBoundedPartitions"
+holes = ["minimal_balanceable_of_bounded"]
+submitter = "Julia M. Himmel"
+source = "https://projecteuler.net/problem=772"