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 · problems.science

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 current result

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

Retained declaration

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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:648
PLBY Lean proofsErdosProblems.Erdos648

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

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

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science