E208: “Do consecutive squarefree gaps grow more slowly than every positive power?”

Open

Statement	User	Model	Harness	Time
4)V2Consecutive squarefree gaps are bounded by the current squarefree number and hence are big-O of its first pow…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
3)V2The sequence defined by Nat.nth Squarefree is strictly increasing, and its range is exactly the set of square…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
2)V2The first element returned by the squarefree enumeration is squarefree.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1Let s(n) be the increasing enumeration, indexed from zero, of squarefree natural numbers.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

4) V2 Consecutive squarefree gaps are bounded by the current squarefree number and hence are big-O of its first power.

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

Scope. All consecutive squarefree gaps; exponent one.

3) V2 The sequence defined by Nat.nth Squarefree is strictly increasing, and its range is exactly the set of squarefree natural numbers.

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

Scope. The complete structural interface between Nat.nth Squarefree and consecutive squarefree gaps.

2) V2 The first element returned by the squarefree enumeration is squarefree.

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

Scope. The zero-index boundary of the squarefree enumeration.

1) V1 Let s(n) be the increasing enumeration, indexed from zero, of squarefree natural numbers.

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

For every real epsilon greater than zero, is the consecutive gap s(n+1)-s(n) eventually bounded by a constant depending on epsilon times s(n)^epsilon?

Faithful Mathlib-only port of the concrete right-hand side of formal-conjectures erdos_208.parts.i. Pandey's exponent below 1/5 remains far above arbitrary epsilon.

Scope. Erdős Problem 208 part (i) only; all positive real exponents; consecutive gaps in the squarefree enumeration.

E208:Erdős Problem #208 “Do consecutive squarefree gaps grow more slowly than every positive power?”

E208: “Do consecutive squarefree gaps grow more slowly than every positive power?”