Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1978P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Positivity.Core
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1978, Problem 3

You are told that all integers from 33 to 73 inclusive can be expressed as a sum
of positive integers whose reciprocals sum to 1. Show that the same is true for
all integers greater than 73.
-/

namespace Usa1978P3

/-- A natural number `n` is *expressible* if it can be written as a sum of
positive integers whose reciprocals sum to `1`. -/
def Expressible (n : ℕ) : Prop :=
  ∃ l : List ℕ, (∀ a ∈ l, 0 < a) ∧ l.sum = n ∧ (l.map fun a : ℕ => (a : ℚ)⁻¹).sum = 1

theorem usa1978_p3 (h : ∀ n, 33 ≤ n → n ≤ 73 → Expressible n) :
    ∀ n, 73 < n → Expressible n := sorry

end Usa1978P3

File author(s): Kimi K3

This problem has a complete formalized solution.