Balanceable k-bounded partitions | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: https://projecteuler.net/problem=772

Informal solution: Unavailable.

theorem declaration uses `sorry`minimal_balanceable_of_bounded (k : ℕ) (hk : 0 < k) :
    Minimal (fun n => 0 < n ∧ ∀ p : n.Partition, LeanEval.Combinatorics.Bounded k p → LeanEval.Combinatorics.Balanceable p) (2 * (Finset.Icc 1 k).lcm id) := byk:ℕhk:0 < k⊢ Minimal (fun n => 0 < n ∧ ∀ (p : n.Partition), Bounded k p → Balanceable p) (2 * (Finset.Icc 1 k).lcm id)
  sorryAll goals completed! 🐙