E371: “Do rising largest prime factors have density one half?”

Open

Statement	User	Model	Harness	Time
2)V2There are infinitely many n for which the largest prime factor rises from n to n+1.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1The set of natural numbers n for which the largest prime factor of n+1 exceeds that of n has natural density…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 There are infinitely many n for which the largest prime factor rises from n to n+1.

kernel-checked, filed Tue Aug 25 2026 05:49:32 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. An unconditional infinitude result toward the density conjecture, using the same largest-prime-factor definition.

1) V1 The set of natural numbers n for which the largest prime factor of n+1 exceeds that of n has natural density 1/2.

open, filed Tue Aug 25 2026 05:49:18 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Full-local mode. Twelve compiling attacks are red for restatement; n=1 concretely witnesses the event; independent transcription is equivalent; clean exact? and direct negation fail. Five targeted searches confirmed the root remains beyond the 0.2017 unconditional lower bound; logarithmic density and almost-all-scales results do not imply ordinary density. Whole routes examined shifted primes, rise/fall/tie decomposition, Dickman independence, sieve bounds, and density symmetry. Lean proves every prime p gives a rising index p−1, hence infinitely many rises, but this zero-density subfamily cannot establish 1/2. No Commons or computational exhaustion.

Scope. The support definitions Nat.maxPrimeFac and Set.HasDensity are inlined exactly from current Formal Conjectures support because they are not yet in Mathlib.

E371:Erdős Problem #371 “Do rising largest prime factors have density one half?”

E371: “Do rising largest prime factors have density one half?”