A competition programming problem about permuting a permutation to be unimodal

permute_to_unimodal

Submitter: Julia M. Himmel.

Notes: Unavailable.

Source: NWERC 2025 Problem G, see https://2025.nwerc.eu/problem-set.pdf

Informal solution: See https://2025.nwerc.eu/solutions.pdf for a sketch of the correctness, which goes in two steps: construct a quadratic-time dynamic programming solution, then efficiently evaluate that in O(n log n). The hard part is showing the correspondence between LISs of prefixes of the constructed sequence and values of the DP.

theorem declaration uses `sorry`minRearrange_correct {arr : Array Nat} :
    arr.Perm (1...=arr.size).toArray →
      (∃ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x ∧ LeanEval.ProgramVerification.differences (Vector.mk x (byarr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size simpa using hx.size_eqAll goals completed! 🐙)) arr.toVector = LeanEval.ProgramVerification.minRearrange arr) ∧
      (∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray), LeanEval.ProgramVerification.Unimodal x → LeanEval.ProgramVerification.minRearrange arr ≤ LeanEval.ProgramVerification.differences (Vector.mk x (byarr:Array Natx:Array Nathx:x.Perm (1...=arr.size).toArray⊢ x.size = arr.size simpa using hx.size_eqAll goals completed! 🐙)) arr.toVector) := byarr:Array Nat⊢ arr.Perm (1...=arr.size).toArray →
  (∃ x hx, Unimodal x ∧ differences (Vector.mk x ⋯) arr.toVector = minRearrange arr) ∧
    ∀ (x : Array Nat) (hx : x.Perm (1...=arr.size).toArray),
      Unimodal x → minRearrange arr ≤ differences (Vector.mk x ⋯) arr.toVector
  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

• @LorenzoLuccioli with Aristotle (Harmonic) on May 20, 2026 (proof)