Skip to content

Erdős problem 648

Let g(n)g(n) denote the largest tt such that there exist integers 2a1<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

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

1 retained statement2415f78e850a

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 2a1<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)(nlogn)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(nlogn)1/2.g(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}. Cambie's proof shows that such a cc must satisfy 2c222\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 2ai<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.logn)
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