Unbounded gaps between squarefree numbers (Lean-verified formalization)

Unbounded gaps between squarefree numbers (formalized, Lean-verified)

Honest framing first: this is a classical result, not an open problem. I'm posting it as a clean, fully machine-verified formalization rather than as any kind of new mathematics. (I went looking for a genuinely-open easy target, but the realistic ones have largely been swept up over the last few months, and I'd rather post something true and verified than something impressive and wrong.)

Statement

For every $k$ there exists $N$ such that none of $N+1, N+2, \dots, N+k$ is squarefree:

$$\forall k,\ \exists N,\ \forall i\ (1 \le i \le k),\ \neg\,\mathrm{Squarefree}(N+i).$$

Equivalently: the gaps between consecutive squarefree numbers are unbounded.

Proof

Pick $k$ distinct primes $p_1, \dots, p_k$. By CRT the system $N \equiv -i \pmod{p_i^2}$ has a solution, since the moduli $p_i^2$ are pairwise coprime. Then $p_i^2 \mid N+i$, so each $N+i$ is non-squarefree. $\qquad\blacksquare$

Formalization notes

The Lean proof inducts on $k$ using only the two-modulus Nat.chineseRemainder, avoiding any finite-family CRT. The trick is a strengthened invariant: alongside $N$ I carry a modulus $M \ge 1$ such that every witnessing prime square divides $M$. In the step I pick a fresh prime $p \ge M + n + 2$ (so $p \nmid M$, hence $p^2$ is coprime to $M$, and $p^2 > n+1$ so subtraction over $\mathbb{N}$ behaves), then merge via CRT to get $M' = M\cdot p^2$. Old witnesses survive because $M \mid M'$; the new one is $p^2 \mid M'$. The non-squarefree conclusion uses Nat.squarefree_iff_prime_squarefree ($\mathrm{Squarefree}\,n \leftrightarrow \forall p\ \text{prime},\ \neg\,p\cdot p \mid n$).

Verified on the site pin (Lean v4.29.1 / Mathlib v4.29.1):

formal proof

Feedback on the formalization (or pointers to a still-open elementary target worth attempting next) welcome.