Balanceable k-bounded partitions

balanceable_bounded_partitions

Submitter: Julia M. Himmel.

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! 🐙

Solved by

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 13, 2026

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026