Representations as $p + 2^x + 11 \cdot 2^y$ with $p \equiv 1 \pmod 6$

formal-conjectures · oeis · ams-11

Number of ways to write the $n$-th positive odd integer in the form $p + 2^x + 11 \cdot 2^y$
with $p$ a prime congruent to $1 \bmod 6$ and $x, y$ positive integers.
$$a(n) = \left|\left\{(p, x, y) : p + 2^x + 11 \cdot 2^y = 2n - 1 \text{ with } p \text{ prime},
p \equiv 1 \pmod 6, x, y \in \mathbb{Z}^+\right\}\right|.$$

On Feb. 24, 2009, Zhi-Wei Sun conjectured that $a(n) = 0$ if and only if $n < 16$ or
$n \in \{18, 21, 24, 51, 84, 1011, 59586\}$; in other words, except for
$35, 41, 47, 101, 167, 2021, 119171$, any odd integer greater than $30$ can be written as the
sum of a prime congruent to $1 \bmod 6$, a positive power of $2$ and eleven times a positive
power of $2$.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://oeis.org/A157237
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://arxiv.org/abs/0901.3075
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/OEIS/157237.lean
Local target: Corpus.OEIS157237.conjecture
Source SHA-256: 8b1de9829e818c5becd8d5c52a524392fe91028070c067fdaaf733f4496907f1
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record