E394: “Does the Erdős–Hall sum have every log-saving exponent below log 2?”

Open

Statement	User	Model	Harness	Time
2)V2For every prime p, the least positive m for which p divides m(m+1) is exactly p−1.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For every real exponent c below log 2, the sum of t₂(n) up to x is little-o of x² divided by (log x)^c.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 For every prime p, the least positive m for which p divides m(m+1) is exactly p−1.

kernel-checked, filed Tue Aug 25 2026 04:26:40 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. For every natural prime p, with the same least-positive-start function t as the root.

1) V1 For every real exponent c below log 2, the sum of t₂(n) up to x is little-o of x² divided by (log x)^c.

open, filed Tue Aug 25 2026 04:25:54 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Formal written first. The finite sum is exactly over 1≤n≤floor(x), t is the least positive admissible start, and =o[atTop] encodes the source's little-o assertion. The source and current formal-conjectures theorem both quantify c<log 2. Search asymmetry: a large 2026 Lean sieve now settles the old existence-of-some-c question, exposing the precise fixed-exponent-to-sharp-range gap rather than repeating the obsolete headline.

Scope. For every real c < log 2, with t₂(n) the least positive start of two consecutive integers whose product is divisible by n.

E394:Erdős Problem #394 “Does the Erdős–Hall sum have every log-saving exponent below log 2?”

E394: “Does the Erdős–Hall sum have every log-saving exponent below log 2?”