[veljjanoski]

This PR adds a new conjecture-checking machine: brocard_28, a 28-state 2-symbol Turing machine
that halts on the blank tape if and only if Brocard's problem n! + 1 = m^2 has a solution with
n > 7, i.e. beyond the known solutions n = 4, 5, 7 (Brocard 1876, 1885; Ramanujan 1913;
Erdős conjectured there are no others; none exist for n ≤ 10^12).

Machine. Everything is unary. The tape holds n cells and n!/8 cells; n! + 1 = m^2
forces m = 2k + 1, so n!/8 = 1 + 2 + ⋯ + k is a triangular number. A round multiplies the
second block by n + 1 (a hole walks through the first block, one copy per cell; at the start of
each round one cell is written left of the first block) and tests the result by subtracting
1, 2, 3, …; the blank beyond the chunk block acts as its hole, so each wrap grows it for free. A
success walks back over the second block counting its ones modulo 4: residue 0 halts, and
since 32 divides n! for n ≥ 8 this is exactly the case n ≥ 8; the known solutions give
15 ≡ 3 and 630 ≡ 2 (mod 4) and return to the next round. The start is a single state that
steers the loop's own states, through its two never-read cells, to write 1111 0 111 in 46 steps
(earlier versions with 41 and 34 states, whose gate counted the cells of the first block, are in
the PR history). Layout and credits: artifacts/brocard_28/README.md.

Proofs (Cryptids/Brocard28.lean, Cryptids/Semantics/Brocard28.lean):

• halts_brocard28_iff_exists_tri : Halts brocard28 ↔ ∃ n, 8 ≤ n ∧ IsTri (n ! / 8) — propext,
  Quot.sound.
• halts_brocard28_iff_exists_square : Halts brocard28 ↔ ∃ n, 7 < n ∧ IsSquare (n ! + 1) —
  propext, Quot.sound (in comparator/constructive.json).
• halts_brocard28_iff_not_brocard : Halts brocard28 ↔ ¬ BrocardConjecture — classical (Markov).

Wiring. Machines.lean, Propositions.lean (BrocardConjecture), Challenge.lean,
comparator/brocard_28.json (+ constructive.json, all.json), verify.py (table and SHA-256
checks against both Lean files, the 46-step start, blank-tape stage checks, a planted triangular
number halts and a non-triangular one reaches the next test with the expected tape), docs and
formalization.yaml.

Prior work. Charlie Reams's 61-state machine with a Lean proof
(calr3/tinycryptids, brocard/, November 2026) and a
43-state table without a machine-checked proof in Tandi, Gonzalez-Hendrix and Brown
(arXiv:2605.20215).
Improving that 43-state count is Open Problem 6.2 in Gasarch's SIGACT News column (Sept 2026), which reports Jonathan Brown's conjecture that about 30 states may suffice.
The design here is different (triangularity of n!/8, in-place multiply, counter grown at each round start, residue gate).

Claude (Anthropic) was used as assistant.

[veljjanoski]

@mo271 this may be a new record for Brocard’s problem :)

[mo271]

Really nice work: getting Brocard's problem down to 28 states (beating both the 61-state proved bound and the 43-state unproved construction, and even clearing the ~30-state conjecture) is a great result! The $n!/8 = T_k$ triangularity test with the free $+1$ chunk wrap, the $\bmod,4$ gate to rule out $n = 5, 7$ since $32 \mid n!$ for $n \ge 8$, and the 1-state GO bootstrap reusing TLx@0 / M1@0 are all super clean.

I checked out the branch locally, ran python3 verify.py --steps 600000, and read through Cryptids/Brocard28.lean, Cryptids/Semantics/Brocard28.lean, Challenge.lean, Cryptids/Propositions.lean, and the comparator configs. Having halts_brocard28_iff_exists_square completely constructive (propext + Quot.sound only) with Markov's Principle isolated to halts_brocard28_iff_not_brocard fits the repo's split nicely.

Only found two tiny stale state-range headers in Cryptids/Brocard28.lean (looks like leftovers from an earlier state count; Gate (States 23–27) on line 738 is already updated):

• Cryptids/Brocard28.lean line 277: /-! ## Multiply (States 8–17) -/ -> States 2–11`` (to match the module docstring and state abbrevs).
• Cryptids/Brocard28.lean line 474: /-! ## Test (States 18–26) -/ -> States 1, 12–22`` (covering Test 1, `12`–`19` and Fail `20`–`22`).

LGTM once those two comments are touched up (or in a quick follow-up)!

[veljjanoski]

thanks, both headers fixed in the follow-up commit