Skip to content

Erdős problem 442

Let Log⁡x:=max⁡{log⁡x,1}\operatorname{Log} x := \max\{\log x, 1\}, Log⁡2x=Log⁡(Log⁡x)\operatorname{Log}_2x = \operatorname{Log} (\operatorname{Log} x), and Log⁡3x=Log⁡(Log⁡(Log⁡x)).\operatorname{Log}_3x = \operatorname{Log}(\operatorname{Log}(\operatorname{Log} x)). Is it true that if A⊆NA\subseteq\mathbb{N} is such that 1Log⁡2x∑n∈A:n≤x1n→∞ \frac{1}{\operatorname{Log}_2 x} \sum_{n\in A: n\leq x} \frac{1}{n}\to\infty then (∑n∈A:n≤x1n)2∑n,m∈A:n<m≤x1lcm⁡(n,m)→∞ \left(\sum_{n\in A: n\leq x} \frac{1}{n}\right)^2 \sum_{n, m \in A: n < m \leq x} \frac{1}{\operatorname{lcm}(n, m)}\to\infty as x→∞x\to\infty?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

442.lean

Retained formal statement2 of 2

Tao resolved erdos_442 in the negative in Theorem 1 of https://arxiv.org/pdf/2407.04226. The following is a formalisation of that theorem with C0=1C_0 = 1.

Let Log⁡x:=max⁡{log⁡x,1}\operatorname{Log} x := \max\{\log x, 1\}, Log⁡2x=Log⁡(Log⁡x)\operatorname{Log}_2x = \operatorname{Log} (\operatorname{Log} x), and Log⁡3x=Log⁡(Log⁡(Log⁡x)).\operatorname{Log}_3x = \operatorname{Log}(\operatorname{Log}(\operatorname{Log} x)). There exists a set AA of natural numbers such that ∑n∈A:n≤x1n=exp⁡(((12+o(1))Log⁡21/2xLog⁡3x)) \sum_{n\in A: n\leq x} \frac{1}{n} = \exp\left(\left(\left(\frac{1}{2} + o(1)\right)\operatorname{Log}_2^{1/2}x \operatorname{Log}_3x\right)\right) and ∑n,m∈A:n,m≤x1lcm⁡(n,m)≪(∑n∈A:n≤x1n)2 \sum_{n, m\in A: n, m\leq x} \frac{1}{\operatorname{lcm}(n, m)}\ll\left(\sum_{n\in A: n\leq x} \frac{1}{n}\right)^2

FormalConjectures/ErdosProblems/442.leanErdos442.erdos_442.variants.tao9 linesExact file
∃ A f C,  ∃ (_ : 0 < C) (_ : f =o[Filter.atTop] 1),    ∀ᶠ (x : ℝ) in Filter.atTop,      ∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n =          Real.exp            ((1 / 2 + f x) * √(Erdos442.Real.maxLogOne (Erdos442.Real.maxLogOne x)) *              Erdos442.Real.maxLogOne (Erdos442.Real.maxLogOne (Erdos442.Real.maxLogOne x))) ∧        |∑ nm ∈ ((A ∩ Set.Icc 1 ⌊x⌋₊) ×ˢ (A ∩ Set.Icc 1 ⌊x⌋₊)).toFinset, 1 / ↑(nm.1.lcm nm.2)| ≤          C * (∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) ^ 2
SolvedStatement only, no proof