Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1981P4

import Mathlib

namespace Imo1981P4

/-!
# International Mathematical Olympiad 1981, Problem 4

(a) For which values of $n>2$ is there a set of $n$ consecutive positive integers such that
the largest number in the set is a divisor of the least common multiple of the remaining $n-1$ numbers?

(b) For which values of $n>2$ is there exactly one set having the stated property?
-/

open Finset

def last_divides_lcm_remaining (n k : ℕ) : Prop := k+n ∣ lcm (Icc (k+1) (k+n-1)) id

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

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

theorem imo1981_p4 (n : ℕ) :
      (n ∈ values_a ↔ 2 < n ∧ ∃  k, last_divides_lcm_remaining n k)
    ∧ (n ∈ values_b ↔ 2 < n ∧ ∃! k, last_divides_lcm_remaining n k) := sorry


end Imo1981P4

File author(s): Constantin Seebach

This problem has a complete formalized solution.