Number theory

Erdős 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

No one has attempted this yet.

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-379fc029-erdos371-erdos-371-abc4596732-formalized-v1
Task commitment: sha256:4bad8b070f9f5c695035dc4cf83bebe3e8ec2754d7f8397cd3ce2c39c95694b9

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.