Skip to content

Erdős problem 1190

Let ϵm=max⁡∑1ni\epsilon_m=\max \sum \frac{1}{n_i} where the maximum is taken over all finite sequences m<n1<⋯<nkm<n_1<\cdots<n_k for which there exist congruences ai(modni)a_i\pmod{n_i} such that no integer satisfies two such congruences.

Sources

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

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1190.lean

Retained formal statement1 of 5

Let ϵm=max⁡∑1ni\epsilon_m=\max \sum \frac{1}{n_i} where the maximum is taken over all finite sequences m<n1<⋯<nkm<n_1<\cdots<n_k for which there exist congruences ai(modni)a_i\pmod{n_i} such that no integer satisfies two such congruences.

Estimate ϵm\epsilon_m.

The resolution of [202] by GPT-5.4 Pro implies via the same reduction that ϵm=L(m)−1+o(1),\epsilon_m=L(m)^{-1+o(1)}, where L(m)=exp⁡(log⁡mlog⁡log⁡m)L(m)=\exp(\sqrt{\log m\log\log m}).

FormalConjectures/ErdosProblems/1190.leanErdos1190.erdos_11902 linesExact file
∀ (ε : ℝ),  0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, scaleL m ^ (-1 - ε) < Erdos1190.eps m ∧ Erdos1190.eps m < scaleL m ^ (-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.

Search problems.science

Find a Problem, Result, source, or page