Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2002P4

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Finset.Sort
public import Mathlib.Data.Rat.Star
public import Mathlib.NumberTheory.Divisors
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.FieldSimp.Lemmas
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Linarith.Preprocessing
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Positivity
public import Mathlib.Tactic.Positivity.Core
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Ring.Basic

public section


/-!
# International Mathematical Olympiad 2002, Problem 4

The positive divisors of the integer n > 1 are d₁ < d₂ < ... < dₖ, so that
d₁ = 1 and dₖ = n. Let d = d₁d₂ + d₂d₃ + ... + dₖ₋₁dₖ.
Show that d < n² and find all n for which d divides n².
-/

namespace Imo2002P4

open Finset

/-- The `i`-th smallest positive divisor of `n` (meaningful for `i < n.divisors.card`). -/
noncomputable def nthDiv (n i : ℕ) : ℕ :=
  if h : i < n.divisors.card then n.divisors.orderEmbOfFin rfl ⟨i, h⟩ else 1

/-- The sum `d₁d₂ + d₂d₃ + ... + dₖ₋₁dₖ` over the ordered positive divisors of `n`. -/
noncomputable def pairSum (n : ℕ) : ℕ :=
  ∑ i ∈ Finset.range (n.divisors.card - 1), nthDiv n i * nthDiv n (i + 1)

/- determine -/ abbrev SolutionSet : Set ℕ := sorry

theorem imo2002_p4 (n : ℕ) (hn : 1 < n) :
    pairSum n < n ^ 2 ∧ (pairSum n ∣ n ^ 2 ↔ n ∈ SolutionSet) := sorry

end Imo2002P4

File author(s): Kimi K3

This problem has a complete formalized solution.