Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2012P4

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Ring.Divisibility.Basic
public import Mathlib.Data.Int.NatAbs
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2012, Problem 4

Find all functions $f : \mathbb{N} \to \mathbb{N}$ such that $f(n!) = f(n)!$ for all
positive integers $n$ and such that $m - n$ divides $f(m) - f(n)$ for all distinct
positive integers $m, n$.
-/

namespace Usa2012P4

open Nat

/-- The conditions of the problem on a function `f : ℕ → ℕ`. Since the problem
is about functions on the positive integers, we require positivity of `f` on
positive inputs explicitly; the value `f 0` is irrelevant. -/
def IsSolution (f : ℕ → ℕ) : Prop :=
  (∀ n, 0 < n → 0 < f n) ∧
    (∀ n, 0 < n → f (n !) = (f n)!) ∧
      ∀ (m n : ℕ), 0 < m → 0 < n → m ≠ n → (m : ℤ) - n ∣ (f m : ℤ) - f n

/-- The answer: the constant functions `1` and `2`, and the identity
(on positive integers). -/
/- determine -/ abbrev solution_set : Set (ℕ → ℕ) := sorry

theorem usa2012_p4 (f : ℕ → ℕ) :
    f ∈ solution_set ↔ IsSolution f := sorry

end Usa2012P4

File author(s): Kimi K3

This problem has a complete formalized solution.