Skip to content

Erdős problem 1188

Estimate the number F(x)F(x) of minimal distinct covering systems whose moduli all lie in [1,x][1, x]. The candidate proof gives log⁡log⁡F(x)/log⁡x→1\log\log F(x)/\log x \to 1, i.e. F(x)=exp⁡(x1+o(1))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.

Retained declaration

FormalConjectures/ErdosProblems/1188.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1188.leanErdos1188.erdos_11881 lineExact file
Filter.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.

Proof manifests naming this Problem

  • William Blair Lean proofswilliamjblair:Research.erdos1188_loglog_ratio_tendsto_one

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • argument

    VibeMathed

    Machine
    GPT-5.6 starships (Claude Fable 5 reviewer)
    Reported outcome
    candidate
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page