Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1976P4

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1976, Problem 4

Determine, with proof, the largest number which is the product
of positive integers whose sum is 1976.
-/

namespace Imo1976P4

/- determine -/ abbrev solution : ℕ := sorry

theorem imo1976_p4 :
    IsGreatest
      { n | ∃ s : Multiset ℕ, s.sum = 1976 ∧ s.prod = n }
      solution := sorry


end Imo1976P4

File author(s): Benpigchu

This problem has a complete formalized solution.