Golden-ratio growth of Conway's subprime closure

Source abstract

Let $s(m)$ be the Conway subprime function define the binary operation on the natural numbers $x \circ y= s(x + y)$, and denote by $C_n$, $n \ge 0$, the sequence of subsets of natural numbers defined by $C_0 = \{1\}$, and $C_{n+1} = C_n \cup (C_n \circ C_n)$. We prove the conjecture by Caragiu, Vicol and Zaki that $$\lim_{n\to \infty} \frac{ | C_{n+1}| }{ | C_n |}= \frac{1+\sqrt{5}}{2}.$$ The underlying mathematical proof in this paper was constructed with some algorithmic assistance from GPT-6 Astra and its correctness has been formally verified using the Lean 4 proof assistant.