Skip to content

Erdős problem 648

Let g(n)g(n) denote the largest tt such that there exist integers 2≤a1<a2<⋯<at<n2\leq a_1<a_2<\cdots <a_t <n such that P(a1)>P(a2)>⋯>P(at)P(a_1)>P(a_2)>\cdots >P(a_t) where P(m)P(m) is the greatest prime factor of mm. Estimate g(n)g(n).

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

648.lean

Retained formal statement1 of 1

Let g(n)g(n) denote the largest tt such that there exist integers 2≤a1<a2<⋯<at<n2\leq a_1<a_2<\cdots <a_t <n such that P(a1)>P(a2)>⋯>P(at)P(a_1)>P(a_2)>\cdots >P(a_t) where P(m)P(m) is the greatest prime factor of mm. Estimate g(n)g(n).

Stijn Cambie has proved [Ca25b] g(n)≍(nlog⁡n)1/2.g(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}. Cambie further asks whether there exists a constant cc such that g(n)∼c(nlog⁡n)1/2.g(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}. Cambie's proof shows that such a cc must satisfy 2≤c≤222\leq c\leq 2\sqrt{2}.

The sequence a1<a2<⋯<ata_1<a_2<\cdots<a_t is packaged as a strictly monotone map a : Fin t → ℕ with 2≤ai<n2\leq a_i<n, the greatest prime factor PP is Nat.maxPrimeFac, and g(n)g(n) is the supremum in ℕ of the achievable lengths tt.

FormalConjectures/ErdosProblems/648.leanErdos648.erdos_6481 lineExact file
(fun n => ↑(Erdos648.g n)) =Θ[Filter.atTop] fun n => √(↑n / Real.log ↑n)
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.