How to formalize the Odd/Distinct Partition Bijection?

Stream: maths

[Brisal]

I want to formalize the theorem "the number of partitions into odd parts equals the number of partitions into distinct parts" in Lean4, aiming to prove it by constructing an explicit bijection in both directions:

For odd partitions, recursively merge repeated odd parts (e.g., 5+5→10) until all parts are distinct; for distinct partitions, recursively split even parts (e.g., 6→3+3) until all parts are odd.

However, I'm unsure how to elegantly implement this recursive operation in Lean4, particularly how to ensure termination and prove the bijection's invertibility. I'd like to ask if there's existing Mathlib support or more efficient implementation approaches. For example, for n=8, how to mutually convert between the odd partition 3+3+1+1 and the distinct partition 6+2?

The #mwe as follow:

import Mathlib
open Finset Nat Std List

theorem partition_odd_eq_distinct (n : ℕ) (h : n > 0):
  Fintype.card (Partition.odds n) = Fintype.card (Partition.distincts n) := by
  unfold Partition.odds Partition.distincts
  simp only [not_even_iff_odd, Finset.mem_filter, mem_univ, true_and]

  let f : {π : Partition n // ∀ x ∈ π.parts, Odd x} → {π : Partition n // π.parts.Nodup} :=
  fun π =>
    sorry

  let g : {π : Partition n // π.parts.Nodup} → {π : Partition n // ∀ x ∈ π.parts, Odd x} :=
  fun π =>
    sorry

  have fg_id : ∀ (π : {π : Partition n // ∀ x ∈ π.parts, Odd x}),
    g (f π) = π := by
    intro π
    sorry


  have gf_id : ∀ (π : {π : Partition n // π.parts.Nodup}),
    f (g π) = π := by
    intro π
    sorry

  have e : {π : Partition n // ∀ x ∈ π.parts, Odd x} ≃
           {π : Partition n // π.parts.Nodup} :=
    { toFun := f, invFun := g, left_inv := fg_id, right_inv := gf_id }
  exact Fintype.card_congr e

[Jakob von Raumer]

Better ask this on #mathlib4 or #Is there code for X?

[Notification Bot]

This topic was moved here from #Machine Learning for Theorem Proving > How to formalize the Odd/Distinct Partition Bijection? by Floris van Doorn.

[Floris van Doorn]

Some comments:

• I would double check the description of your solution: I don't think that gives a bijection (EDIT: Oh, I think it's probably right, I just misunderstood)
• In Lean, I recommend first definition your functions f and g using def, before starting your theorem.
• Even better that, maybe just define the functions with type Partition n -> Partition n, and afterwards prove that they have the right properties.

[Brisal]

Jakob von Raumer said:

Better ask this on #mathlib4 or #Is there code for X?

Well thank you

[Bhavik Mehta]

Here's how I formalised it a while ago: https://leanprover-community.github.io/mathlib4_docs/Archive/Wiedijk100Theorems/Partition.html.

[Chi-Yun Hsu]

@Risal My two students and I are working on the formalization of this right now. To define the map from odd partitions to distinct partitions, "recursively merge repeated odd parts" is equivalent to "write the multiplicity of an odd parts in binary expansion, and each product of a power of 2 and the odd part gives a part in the corresponding distinct partition". We used Nat.bitIndices to implement the map from odd partitions into partitions, as below.

def binary (n : ℕ): Multiset ℕ := n.bitIndices.map fun i => 2 ^ i

def FromOdd_parts (n : ℕ) (P : n.Partition) (_ : P ∈ (odds n)): Multiset ℕ :=
   ∑ a ∈ P.parts.toFinset, (binary (Multiset.count a P.parts)).map (fun y ↦ y * a)

There are quite some details needed to formalize since a partition of n is a structure consisting of the multiset of natural numbers, proofs that each part is positive, and that the sum of parts is n. We have finished these, but are still working on showing the resulting partition is indeed distinct. We are also half way through formalizing the inverse map from distinct partitions to odd partitions.