Erdős problem 1188 · problems.science

Estimate the number $F(x)$ of minimal distinct covering systems whose moduli all lie in $[1, x]$ . The candidate proof gives $\log\log F(x)/\log x \to 1$ , i.e. $F(x) = \exp(x^{1+o(1)})$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1188.lean

Retained formal statement1 of 1

Call a set of distinct integers $1<n_1<\cdots<n_k$ with associated congruence classes $a_i\pmod{n_i}$ a distinct covering system if every integer satisfies at least one of these congruences. A minimal distinct covering system is one such that no proper subset forms a covering system. Let $F(x)$ count the number of minimal distinct covering systems with all moduli in $[1,x]$ . Estimate $F(x)$ .

The estimate is log(log F(x)) / log x → 1.

FormalConjectures/ErdosProblems/1188.leanErdos1188.erdos_11881 lineExact file

1Filter.Tendsto (fun x => Real.log (Real.log ↑(Erdos1188.coveringCount x)) / Real.log ↑x) Filter.atTop (nhds 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.

Sources

Search problems.science