Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2025P4

import Mathlib

/-!
# International Mathematical Olympiad 2025, Problem 4

A proper divisor of a positive integer N is a positive divisor of N other
than N itself. The infinite sequence a₁, a₂, ... consists of positive integers,
each of which has at least three proper divisors. For each n ⩾ 1, the integer
aₙ₊₁ is the sum of the three largest proper divisors of aₙ. Determine all
possible values of a₁.
-/

namespace Imo2025P4

open Finset

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

theorem imo2025_p4 : {a₁ | ∃ a : ℕ → ℕ, a 0 = a₁ ∧ ∀ i, 0 < a i ∧ 3 ≤ #(Nat.properDivisors (a i)) ∧
    a (i + 1) = (((Nat.properDivisors (a i)).sort (· ≤ ·)).reverse.take 3).sum} = answer := sorry

end Imo2025P4

File author(s): Joseph Myers, Markus Rydh

This problem does not yet have a complete formalized solution.

The problem was imported from IMOLean/IMO/IMO2025P4.lean.