a(n) is the integer whose decimal digits are the first n+1 decimal digits of π

Wolfgang Haken (1977) conjectured that no term of this sequence is a perfect square, and estimated the probability that this conjecture is false to be smaller than 10^-9.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Start working on it Submit a claim Follow

Cite

@misc{cairn-oeis-11545,
  title        = {a(n) is the integer whose decimal digits are the first n+1 decimal digits of π},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/oeis-11545}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-29}
}

Also: CITATION.cff · Atom feed of results

Claims

Verified

Disputed

Refuted

On the literature board

The problem

The question

conjecture1. Wolfgang Haken (1977) conjectured that no term of this sequence is a perfect square, and estimated the probability that this conjecture is false to be smaller than $1 0^{-} 9$ .

conjecture2. Number of collisions occurring in a system consisting of an infinitely massive, rigid wall at the origin, a ball with mass m stationary at position $x_{1} > 0$ , and a ball with mass $(1 0^{2} n) m$ at position $x_{2} > x_{1}$ and rolling toward the origin, assuming perfectly elastic collisions and no friction.

Strictly speaking, this property, which is equivalent to the statement that the interval $(mπ, π / arctan (1/ m))$ does not contain an integer for all $m = 1 0^{n}$ , is not known to be true for sure. In other words, we do not know for certain that A332045 does not contain a power of $10$ .

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OEIS.«11545» (2 statements).

theorem conjecture1 : ∀ n, ¬ IsSquare (a n)

theorem conjecture2 :
    ∀ n : ℕ, ¬ ∃ (k : ℤ),
      (Real.pi * (10 : ℝ) ^ n.cast < k.cast) ∧
      (k.cast < Real.pi / Real.arctan (1 / (10 : ℝ) ^ n.cast))

What counts as progress

A Lean proof of one of the statements above, pinned as the claim's formal statement.
Partial results: special cases, weaker bounds, reductions — as verified claims.
Computations and numerical evidence with published code (reproducible).
Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

A011545

Source and licence

Imported from Formal Conjectures (OEIS), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.