Erdős problem 370 · problems.science

Are there infinitely many $n$ such that the largest prime factor of $n$ is $< n^{\frac{1}{2}}$ and the largest prime factor of $n + 1$ is $< (n + 1)^{\frac{1}{2}}$ .

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

370.lean

Retained formal statement1 of 1

Are there infinitely many $n$ such that the largest prime factor of $n$ is $< n^{\frac{1}{2}}$ and the largest prime factor of $n + 1$ is $< (n + 1)^{\frac{1}{2}}$ .

Steinerberger has pointed out this problem has a trivial solution.

This was formalized in Lean by Alexeev using Aristotle.

FormalConjectures/ErdosProblems/370.leanErdos370.erdos_3701 lineExact file

1True ↔ {n | ↑n.maxPrimeFac < √↑n ∧ ↑(n + 1).maxPrimeFac < √(↑n + 1)}.Infinite

SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science