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…