Are there $n$ such that there is a covering system with moduli the divisors of $n$ which is 'as disjoint as possible'? That is, for all $d ∣ n$ with $d > 1$ there is an associated $a_{d}$ such that every integer is congruent to some $a_{d} (mod d)$ , and if there is some integer $x$ with $x \equiv a_{d} (mod d) and x \equiv a_{d^{'}} (mod d^{'})$ then $(d, d^{'}) = 1$ .

Worked, still open.

covering systems · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 5 · solved (literature)

theorem erdos_204 : answer(False) ↔ ∃ (n : ℕ) (a : ℕ → ℤ),
    let D := {d : ℕ | d ∣ n ∧ d > 1}
    (∀ x : ℤ, ∃ d ∈ D, x ≡ a d [ZMOD d]) ∧
    (∀ d ∈ D, ∀ d' ∈ D, d ≠ d' → (∃ x : ℤ, x ≡ a d [ZMOD d] ∧ x ≡ a d' [ZMOD d']) →
      Nat.gcd d d' = 1)

formal-conjectures/204.lean ↗

status

solved

formal

status

Search Vela