1. FormalConjectures
  2. OEIS
  3. «267581»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Recurrence for Rule 167 cellular automaton sequence

Decimal representation of the middle column of the "Rule 167" elementary cellular automaton starting with a single ON (black) cell.

References:

    A267581

    arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.

namespace OeisA267581open Nat Int

The rule function for Rule 167. Inputs must be 0 or 1.

def caRule167 (c_L c_C c_R : ℕ) : ℕ := let R : ℕ := 167 let index : ℕ := 4 * c_L + 2 * c_C + c_R -- Rule 167 is determined by the index-th bit of R. (R / (2 ^ index)) % 2

The state of the Rule 167 elementary cellular automaton at time $t$ and position $x$. The initial condition is a single ON cell at $x=0$. $C(t, x)$ is structurally recursive on $t$.

def caState (t : ℕ) (x : ℤ) : ℕ := match t with | 0 => if x = 0 then 1 else 0 | t' + 1 => let C_t' (y : ℤ) := caState t' y caRule167 (C_t' (x - 1)) (C_t' x) (C_t' (x + 1))

The sequence of bits forming the middle column of the CA pattern, $C_{t, 0}$.

def middleColumnBit (t : ℕ) : ℕ := caState t 0

Decimal representation of the middle column of the "Rule 167" elementary cellular automaton starting with a single ON (black) cell. The term $a(n)$ is the decimal value of the binary number $C_{0, 0} C_{1, 0} \dots C_{n, 0}$, where $C_{i, 0}$ is the state of the center cell at time $i$. $$a(n) = \sum_{k=0}^n C_{k, 0} \cdot 2^{n-k}$$

def a (n : ℕ) : ℕ := Finset.sum (Finset.range (n + 1)) fun k => (middleColumnBit k) * (2^ (n - k))

The floor term in the conjectured recurrence relation for A267581. This term, $\lfloor (1/2)^{(2^{n+1} \bmod n)} \rfloor$, simplifies to 1 if $(2^{n+1} \bmod n) = 0$ (i.e., $n \mid 2^{n+1}$), and 0 otherwise. Since the recurrence is only stated for $n \ge 2$, the $n=0$ case is irrelevant to the conjecture.

def oeisFloorTerm (n : ℕ) : ℕ := if n = 0 then 0 else if (2 ^ (n + 1)) % n = 0 then 1 else 0@[category test, AMS 11] lemma a_0 : a 0 = 1 := ⊢ a 0 = 1 All goals completed! 🐙@[category test, AMS 11] lemma a_1 : a 1 = 3 := ⊢ a 1 = 3 All goals completed! 🐙@[category test, AMS 11] lemma a_2 : a 2 = 6 := ⊢ a 2 = 6 All goals completed! 🐙@[category test, AMS 11] lemma a_3 : a 3 = 13 := ⊢ a 3 = 13 All goals completed! 🐙@[category test, AMS 11] lemma a_4 : a 4 = 26 := ⊢ a 4 = 26 All goals completed! 🐙

Conjecture: $a(n) = 2 a(n-1) + 1 - \lfloor (1/2)^{2^{n+1} \bmod n} \rfloor$ for $n \ge 2$. - Andres Cicuttin, Mar 29 2016

A formal proof has been found with the methods described in arxiv/2605.22763.

@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/267581.wip.lean#L190"] theorem a_recurrence (n : ℕ) (hn : 2 ≤ n) : a n = 2 * a (n - 1) + 1 - oeisFloorTerm n := n:ℕhn:2 ≤ n⊢ a n = 2 * a (n - 1) + 1 - oeisFloorTerm n All goals completed! 🐙end OeisA267581