Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1986P5

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Combinatorics.Enumerative.Partition.Basic

public section


/-!
# USA Mathematical Olympiad 1986, Problem 5

A partition of n is an increasing sequence of integers with sum n.
For example, the partitions of 5 are: 1, 1, 1, 1, 1; 1, 1, 1, 2; 1, 1, 3;
1, 4; 5; 1, 2, 2; and 2, 3. If p is a partition, f(p) = the number of 1s
in p, and g(p) = the number of distinct integers in the partition.
Show that ∑ f(p) = ∑ g(p), where the sum is taken over all partitions of n.
-/

namespace Usa1986P5

theorem usa1986_p5 (n : ℕ) :
    ∑ p : Nat.Partition n, p.parts.count 1 =
      ∑ p : Nat.Partition n, p.parts.toFinset.card := sorry

end Usa1986P5

File author(s): Kimi K3

This problem has a complete formalized solution.