From 96dd37f45be7c8e94be134185fdb3d98e9048792 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 6 May 2026 10:16:13 +0200
Subject: [PATCH 1/3] feat: balanceable k-bounded partitions

---
 .../BalanceableBoundedPartitions.lean         | 37 +++++++++++++++++++
 manifests/problems.toml                       |  9 +++++
 2 files changed, 46 insertions(+)
 create mode 100644 LeanEval/Combinatorics/BalanceableBoundedPartitions.lean

diff --git a/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean b/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean
new file mode 100644
index 0000000..a9af0bd
--- /dev/null
+++ b/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 : Nat} (k : Nat) (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 : Nat} (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_boundedImpliesBalanceable (k : Nat) (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
diff --git a/manifests/problems.toml b/manifests/problems.toml
index d0d66c4..c32e871 100644
--- a/manifests/problems.toml
+++ b/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_boundedImpliesBalanceable"]
+submitter = "Julia M. Himmel"
+source = "https://projecteuler.net/problem=772"
\ No newline at end of file

From f53261d16086d7ded397159799c79b5ea21953e9 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 6 May 2026 10:25:17 +0200
Subject: [PATCH 2/3] style

---
 LeanEval/Combinatorics/BalanceableBoundedPartitions.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean b/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean
index a9af0bd..677ffc1 100644
--- a/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean
+++ b/LeanEval/Combinatorics/BalanceableBoundedPartitions.lean
@@ -11,7 +11,7 @@ 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 : Nat} (k : Nat) (p : n.Partition) : Prop :=
+def Bounded {n : ℕ} (k : ℕ) (p : n.Partition) : Prop :=
   ∀ i ∈ p.parts, i ≤ k
 
 /--
@@ -21,7 +21,7 @@ the same size.
 For example, `12 = (3 + 2 + 1) + (2 + 2 + 2)` is a balanceable partition
 of `12`.
 -/
-def Balanceable {n : Nat} (p : n.Partition) : Prop :=
+def Balanceable {n : ℕ} (p : n.Partition) : Prop :=
   ∃ s₁ s₂, s₁ + s₂ = p.parts ∧ s₁.sum = s₂.sum
 
 /--
@@ -29,7 +29,7 @@ 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_boundedImpliesBalanceable (k : Nat) (hk : 0 < k) :
+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
 

From 4877d28dc638dfd435506a5bf1be75508210aa04 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Wed, 6 May 2026 10:25:34 +0200
Subject: [PATCH 3/3] Adjust manifest

---
 manifests/problems.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/manifests/problems.toml b/manifests/problems.toml
index c32e871..7b4f2ad 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -651,6 +651,6 @@ id = "balanceable_bounded_partitions"
 title = "Balanceable k-bounded partitions"
 test = false
 module = "LeanEval.Combinatorics.BalanceableBoundedPartitions"
-holes = ["minimal_boundedImpliesBalanceable"]
+holes = ["minimal_balanceable_of_bounded"]
 submitter = "Julia M. Himmel"
 source = "https://projecteuler.net/problem=772"
\ No newline at end of file