All-Russian Regional Preparation NT Exercise 2

Is it possible to arrange $2019$ positive integers in a circle so that for every two neighboring integers, one of them is equal to the other multiplied by some prime?

Replace sorry in the template below with your solution. See Answer Bank for acceptible answer declarations. Mathlib version used by the checker is v4.29.0.

import Mathlib.Data.Nat.Prime.Defs

def answer : Prop := sorry

theorem solution : (∃ a : Fin 2019 → ℕ,
    ∀ i, a i > 0 ∧ ∃ p, p.Prime ∧ (a i = p * a (i + 1) ∨ a (i + 1) = p * a i)) ↔ answer := sorry

Submit Solution

Login to submit a solution.

Recent Submissions