For statistical reasons it is conjectured that the sequence is finite. This is formalized as the assertion that for large enough $n$, no valid zeroless power exists, which in our definition results in $a(n) = 0$.

Exact retained declaration excerpt — not the whole file.

/--
For statistical reasons it is conjectured that the sequence is finite.
This is formalized as the assertion that for large enough $n$, no valid zeroless power exists,
which in our definition results in $a(n) = 0$.
-/
@[category research open, AMS 11]
theorem conjecture : ∃ N : ℕ, ∀ n : ℕ, n > N → a n = 0 := by
  sorry