Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1992P3

module

public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Finset.Powerset
public import Mathlib.Order.Interval.Finset.Nat
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1992, Problem 3

A set of 11 distinct positive integers has the property that we can find a
subset with sum n for any n between 1 and 1500 inclusive. What is the smallest
possible value for the second largest element?
-/

namespace Usa1992P3

/--
Formalization of "a set of 11 distinct positive integers such that every
integer between 1 and 1500 is the sum of a subset", with the elements listed
in increasing order as `a 0 < a 1 < … < a 10`.
-/
def Good (a : ℕ → ℕ) : Prop :=
  (∀ i : ℕ, i < 11 → 0 < a i) ∧
  (∀ i : ℕ, i < 10 → a i < a (i + 1)) ∧
  ∀ n : ℕ, 1 ≤ n → n ≤ 1500 → ∃ t : Finset ℕ, t ⊆ Finset.range 11 ∧ ∑ i ∈ t, a i = n

/-- The answer to the problem. -/
/- determine -/ abbrev answer : ℕ := sorry

theorem usa1992_p3 : IsLeast {x : ℕ | ∃ a : ℕ → ℕ, Good a ∧ x = a 9} answer := sorry

end Usa1992P3

File author(s): Kimi K3

This problem has a complete formalized solution.