Let $g(n)$ denote the largest $t$ such that there exist integers $2\leq a_1 P(a_2)>\cdots >P(a_t)$$ where $P(m)$ is the greatest prime factor of $m$. Estimate $g(n)$.

Erdős problem 648

Let $g(n)$ denote the largest $t$ such that there exist integers $2\leq a_1<a_2<\cdots <a_t <n$ such that $P(a_1)>P(a_2)>\cdots >P(a_t)$ where $P(m)$ is the greatest prime factor of $m$ . Estimate $g(n)$ .

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/648.lean

Formal Conjectures

FormalConjectures/ErdosProblems/648.leanErdos648.erdos_6481 lineExact file

1(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.

Reported by these sources. Not reviewed here.

Formalization
Erdős AI contributions wiki · 4 Feb, 2026
Machine
Aristotle
Open the source record