Number theory · Last catalog review 26 Jul 2026

Erdős Problem 371

Let

P(n)

denote the largest prime factor of

n

. Show that the set of

n

with

P(n+1) > P(n)

has density

\frac{1}{2}

References

erdosproblems.com/371

Published 27 Jul 2026Never attempted

Formal statement

Lean type

{n | (n + 1).maxPrimeFac > n.maxPrimeFac}.HasDensity (1 / 2)

What you must prove

import FormalConjectures.ErdosProblems.«371»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos371.erdos_371" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/371.lean

Source type SHA-256: sha256:3664c31ed73005e1596d77d8def95d6bf93c45cefc30d3f1c34a1324337ab9ad
Task id: fc-e923379e-erdos371-erdos-371-0dcceb322a-formalized-v1
Task commitment: sha256:03bba7a97e88b9b137f9841621d3c8ced8720d368d6e9f92bc79111a07006619

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.