Erdős problem 1188

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)})$ .

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/1188.lean

Formal Conjectures

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.

William Blair Lean proofswilliamjblair:Research.erdos1188_loglog_ratio_tendsto_one

Reported by these sources. Not reviewed here.