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 formalization occurrence from the upstream source collection.

Tracked question

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

Lean declaration

theorem conjecture : ∃ N : ℕ, ∀ n : ℕ, n > N → a n = 0