Erdős problem 204

Are there $n$ such that there is a covering system with moduli the divisors of $n$ which is 'as disjoint as possible'?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

204.lean

Retained formal statement1 of 1

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\mid n$ with $d>1$ there is an associated $a_d$ such that every integer is congruent to some $a_d\pmod{d}$ , and if there is some integer $x$ with $x\equiv a_d\pmod{d}\textrm{ and }x\equiv a_{d'}\pmod{d'}$ then $(d,d')=1$ .

The density of such $n$ is zero. Erdős and Graham believed that no such $n$ exist.

Adenwalla [Ad25] has proved there are no such $n$ .

This was formalized by van Doorn in Lean using Aristotle.

FormalConjectures/ErdosProblems/204.leanErdos204.erdos_2045 linesExact file

1False ↔2  ∃ n a,3    have D := {d | d ∣ n ∧ d > 1};4    (∀ (x : ℤ), ∃ d ∈ D, x ≡ a d [ZMOD ↑d]) ∧5      ∀ d ∈ D, ∀ d' ∈ D, d ≠ d' → (∃ x, x ≡ a d [ZMOD ↑d] ∧ x ≡ a d' [ZMOD ↑d']) → d.gcd d' = 1

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.