[veljjanoski]

Closes #15.

Adds Tristan Stérin and Damien Woods's 15-state, 2-symbol machine from
arXiv:2107.12475 and proves that it halts on the blank tape if
and only if Erdős's conjecture on powers of two is false: some 2 ^ n with n > 8 has no digit
2 in base 3 (Erdős, Math. Mag. 52 (1979)). Their correctness proof is on paper; as far as I
know this is the first Lean proof.

theorem halts_erdos15_iff_exists_counterexample :
    Halts erdos15 ↔ ∃ n : ℕ, 8 < n ∧ 2 ∉ Nat.digits 3 (2 ^ n)
theorem halts_erdos15_iff_not_erdosPowersOfTwo :
    Halts erdos15 ↔ ¬ ErdosPowersOfTwoConjecture

with ErdosPowersOfTwoConjecture := ∀ n : ℕ, 8 < n → 2 ∈ Nat.digits 3 (2 ^ n) in
Propositions.lean and Challenge.lean.

It also adds Tristan Stérin's 14-state machine for the same conjecture as a 15 → 14 reduction
(see below).

Proof (erdos_15)

The proof is about the 15-state machine directly; there is no 4-symbol helper machine. At the
start of each pass the tape holds the base-3 digits of 2 ^ n (two cells per digit) and a counter
of how many of 2 ^ 0, …, 2 ^ n have no digit 2. One lemma per routine (doubling, scanning for
a 2, rewinding, incrementing the counter) takes the machine from one pass to the next, so the
machine halts exactly at the fourth power without a digit 2; the first three are 2 ^ 0, 2 ^ 2
and 2 ^ 8.

The core result, halts_erdos15_iff_exists_free in Cryptids/Erdos15.lean, states this with
pw n, the digit list of 2 ^ n computed by repeated doubling, and uses only propext and
Quot.sound. Cryptids/Semantics/Erdos15.lean proves pw n = Nat.digits 3 (2 ^ n). That step
needs Classical.choice, because Nat.digits itself uses it, and the negated form also uses
Markov's Principle (not_forall), as for ¬ GoldbachConjecture. So the two Challenge theorems are
checked in all.json and the new erdos_15.json, not in constructive.json.

erdos_14: Stérin's 14-state machine (15 → 14)

Tristan Stérin
announced
a 14-state machine for the same conjecture on the bbchallenge Discord in October 2026; the
Cryptids page of the
bbchallenge wiki lists it as not independently verified:

1LB1RA_1LC1LB_0RD0RA_1LM0RE_1LF1RE_0LJ1LG_1RK0LH_1RI1LH_0LJ0RE_0RD1LJ_0LL1RK_1RN0LC_0LN---_0RK0LM

It is added in artifacts/erdos_14/ as a reduction of erdos_15, in the same format as
riemann_104 → riemann_95:

theorem candidate_fewer_states : candidate.states < reference.states
theorem candidate_equivalent : Halts candidate ↔ Halts reference
theorem halts_candidate_iff_not_erdosPowersOfTwo :
    Halts candidate ↔ ¬ ErdosPowersOfTwoConjecture

with candidate = erdos14 and reference = erdos15. The machine keeps 2 ^ n in unary and reads
its base-3 digits by repeated division by 3; a single 0 in the block marks where the quotient
ends. One lemma per routine (a division round and its three outcomes, the return to the start, the
counter, the doubling of the block) gives Halts erdos14 ↔ ∃ n, 8 < n ∧ 2 ∉ pw n
(Cryptids/Erdos14.lean), and candidate_equivalent follows from the same statement for
erdos15. Both use only propext and Quot.sound, so candidate_fewer_states and
candidate_equivalent are added to constructive.json; all three theorems are in all.json and
the new erdos_14.json.

Machine tables

The upstream erdos_15 file is not in any format verify.py already reads, so:

• baselines/sources/erdos_15_sterin_woods.txt: the authors' file, verbatim
  (tcosmo/bbsim machines/powers_of_two_15_2.txt at
  3f655ba2c73b, mirrored at docs.bbchallenge.org).
• baselines/tables/erdos_15.txt: the compiled table (start state → 0, other states in order of
  appearance, blank b → 0, a → 1), loaded by Machines.erdos15.
• artifacts/erdos_14/machine.txt: the wiki table with the states A–N numbered 0–13,
  loaded by Machines.erdos14.
• verify.py:
  • a bbsim parser that re-derives the erdos_15 table from the source and checks it against
    the pinned SHA-256s and the Lean definition;
  • a 250,000-step simulation that checks, at every erdos_15 pass, the digits of 2 ^ k and
    the counter (passes k < 425), and that (14, 1) is the only halting entry;
  • SHA-256 and table checks for erdos_14, and a simulation that checks the whole tape at every
    entry to its division state D against the configurations in the proof (21 entries, up to the
    start of the stage for 2 ^ 9, past both counter steps).

Answers to the questions in #15

I made these choices; happy to change any of them:

1. Statement: ErdosPowersOfTwoConjecture as above, with Nat.digits.
2. No Machine 5 4 helper; the proof follows the 15-state table directly.
3. Names: erdos_15 (files, baseline), Machines.erdos15, namespace Erdos15.

One change from the plan in #15: the erdos_15 table lives in baselines/, like riemann_120,
not in artifacts/, since it is a published machine, not a new reduction. erdos_14 is in
artifacts/, as a reduction like riemann_95.

Docs

Cryptids.lean, README.md, Cryptids/README.md, Cryptids/Semantics/README.md (§6, §7),
RELATED_WORK.md (new §4), baselines/PROVENANCE.md, comparator/README.md and
formalization.yaml are updated for both machines and the five new theorems (27 in total).

Verification

Run on Linux (Ubuntu 24.04 in Docker, Lean v4.35.0-rc4, LEAN_NUM_THREADS=1), the steps of
lean_action_ci.yml plus the two per-machine comparator configs:

lake build Cryptids Challenge                           # passes; only the expected sorry warnings in Challenge.lean
lake comparator --config comparator/constructive.json   # Your solution is okay!
lake comparator --config comparator/all.json            # Your solution is okay!
lake comparator --config comparator/erdos_15.json       # Your solution is okay!
lake comparator --config comparator/erdos_14.json       # Your solution is okay!
python3 verify.py                                       # all checks pass

A question

Would you like the constructive erdos_15 core in the Challenge too? That would mean adding dbl
and pw to Challenge.lean and halts_erdos15_iff_exists_free to constructive.json. I left it
out to keep Challenge.lean on Mathlib definitions only.

AI-usage disclosure: Claude (Anthropic) was used as assistant.

[veljjanoski]

I've added Tristan Stérin's 14-state machine for the same conjecture as a 15 → 14 reduction (artifacts/erdos_14, Cryptids/Erdos14.lean), and merged main to fix two README conflicts with #18. The description is updated.