FormalConjectures/ErdosProblems/202.lean
Explanation legend Lean4 Domain Explanation Language (L4DEL)
L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.
- L4DEL
- Lean4 Domain Explanation Language
Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1
3 declarations, 2 contain sorry, 0 declared as axioms
Erdős Problem 202
References:
- erdosproblems.com/202
- [BFV13] de la Bretèche, Régis and Ford, Kevin and Vandehey, Joseph, On non-intersecting arithmetic progressions. Acta Arith. (2013), 381-392.
- [Ch05] Chen, Yong-Gao, On disjoint arithmetic progressions. Acta Arith. (2005), 143-148.
- [Cr03b] Croot, III, Ernest S., On non-intersecting arithmetic progressions. Acta Arith. (2003), 233-238.
- [ErSz68] Erdős, P. and Szemerédi, E., On a problem of P. Erdős and S. Stein. Acta Arith. (1968), 85-90.
- [PaPh24] Park, Jinyoung and Pham, Huy Tuan, A proof of the Kahn-Kalai conjecture. J. Amer. Math. Soc. (2024), 235-243.
Imports (1)
- def
Erdos202.ff Nis the maximum possiblersuch that there are moduli $n_1<\cdots<n_r\leq N$ with associated residues $a_i\pmod{n_i}$ whose congruence classes are disjoint line 46 sourceSource documentation
f Nis the maximum possiblersuch that there are moduli $n_1<\cdots<n_r\leq N$ with associated residues $a_i\pmod{n_i}$ whose congruence classes are disjoint.standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses:
NatProof uses:
SupSet.sSup,Set.ofPred,Exists,Fin,Int,And,StrictMono,LT.lt,OfNat.ofNat,LE.le,Int.ModEq,Eq9 instances, coercions and auxiliary constants left out.
noncomputable def f (N : ℕ) : ℕ := …
- theorem
Erdos202.erdos_202Documented declaration: erdos_202 sorry line 63 sourceSource documentation
Let $n_1<\cdots < n_r\leq N$ with associated $a_i\pmod{n_i}$ such that the congruence classes are disjoint (that is, every integer is $\equiv a_i\pmod{n_i}$ for at most one $1\leq i\leq r$). How large can $r$ be in terms of $N$?
Let $f(N)$ be the maximum possible $r$, and let $L(N)=\exp(\sqrt{\log N\log\log N})$.
This was proved by GPT-5.4 Pro (prompted by Ho Boon Suan), using the argument of [BFV13] together with the resolution of the Kahn-Kalai conjecture by Park and Pham [PaPh24], so that $$f(N)= N L(N)^{-1+o(1)}.$$
depends on sorry what this means
Statement uses:
Exists,Nat,Real,And,Asymptotics.IsLittleO,Filter.atTop,OfNat.ofNat,Filter.Eventually,Eq, Erdos202.f,HMul.hMul,HPow.hPow, scaleL,HAdd.hAdd,Neg.negProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous29 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem erdos_202 : ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ᶠ N : ℕ in atTop, (f N : ℝ) = (N : ℝ) * scaleL N ^ (-1 + o N) := by …Mentions: Erdos202.f, scaleL
- theorem
Erdos202.erdos_202.variants.erdos_szemerediErdős and Stein conjectured that $f(N)=o(N)$, which was proved by Erdős and Szemerédi [ErSz68] sorry line 71 sourceSource documentation
Erdős and Stein conjectured that $f(N)=o(N)$, which was proved by Erdős and Szemerédi [ErSz68].
depends on sorry what this means
Statement uses:
Asymptotics.IsLittleO,Nat,Real,Filter.atTop, Erdos202.fProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous,OfNat.ofNat9 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem erdos_202.variants.erdos_szemeredi : (fun N => (f N : ℝ)) =o[atTop] (fun N : ℕ => (N : ℝ)) := by …Mentions: Erdos202.f