znams_problem
Provedalgebracombinatoricsdivisibilitynumber-theory
Znám's Problem: For every , does there exist a set of positive integers such that each divides ?
Štefan Znám posed this in 1975. Solutions are known for . Example for : since and . The question is whether solutions exist for all . Closely related to Egyptian fraction representations and Sylvester sequences.
Source: Znám, Š. (1975). J. Number Theory 7, 303–310. Also: Sun, Z.W. (2009). On Znám's problem and generalized Znám's problem. Integers 9, A44.
Preamble
import Mathlib
Formal statement
theorem znams_problem (k : ℕ) (hk : 2 ≤ k) :
∃ s : Fin k → ℕ,
(∀ i, 0 < s i) ∧
∀ i, s i ∣ (1 + ∏ j ∈ Finset.univ.erase i, s j) := by
sorrySource