## 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 : Finset ℕ, ∑ i ∈ s, i = 1976 ∧ ∏ i ∈ s, i = n }
solution := sorry
end Imo1976P4
```

This problem does not yet have a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org: