Holdout list 740: what changed for us (2026-10-10)
New list: data/holdouts/BB6_holdouts_740.txt (740 machines, sha1 0aedc3e4…). Compared with the 778 list (2026-10-07_778.txt) we have worked from: 38 removed, 0 added. The 740 machines that remain keep their order.
Headline
- #2 is officially solved. PR #14 was merged by ccz181078 at 13:47 PDT today (merge commit
9cf9e88, fileverify/BellEatsCounter_1RB0RF.v), with no comments and no changes requested. It is the only removal that comes from our work. (That is the "solved very recently" machine: it was on the 815 list and the 778 list, and it is gone from the 740 list because of our PR.) - Our 11 unsubmitted kills are all still on the list, so each still counts once submitted.
- No one solved a machine we are working on. The only other machine of ours that left the list is #19, which we had parked. It left by equivalence, not by a proof (see below).
- The framework did not change. Upstream added 6 new files and edited none, so our proofs, checked against
0940bb9, compile unchanged against the new HEAD9cf9e88.
The 38 removals, by cause
Upstream commit d3c52f5 ("add ChaoticBell1Halt, CubicMachines_v2, Cubic50, Eqv_WordPairs, Eqv_RegularPairs", today 13:23 PDT) plus our merge:
| cause | count | file |
|---|---|---|
| solved by us | 1 | BellEatsCounter_1RB0RF.v (#2) |
| solved upstream: Cubic machines | 4 | CubicMachines_v2.v (3, non-halting), Cubic50.v (1, halts) |
| solved upstream: Chaotic Bell | 2 | ChaoticBell1Halt.v (both halt) |
| removed by equivalence, not solved | 31 | Eqv_WordPairs.v, Eqv_RegularPairs.v |
The 31 equivalence removals are deduplication. Each file proves two holdouts have the same halting behaviour ("neither machine's halting behavior is decided"), and only one representative stays on the list. They do not reduce the real problem count. They also mean that a proof for a representative now covers its removed partners automatically.
None of the 7 really solved machines was on our targeting pool, reserve, watchlist or family sweep. One of them (1RB0RE_1RC0LD_1LD0RF_0LB0LA_1LC1RE_---0RE) was on dyuan01's longitudinal list. The upstream activity is in Cubic and Chaotic Bell. Our classes (Bell eats counter, Skelet 1-like Class 2, Sync bouncer counter, Counter Class 4) saw no competing kills.
Our machines, one by one
| machine | before | 740 list | effect |
|---|---|---|---|
#2 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- |
KILLED, PR #14 open | removed (merged) | done; status.json records the merge |
#19 1RB1RF_1RC---_1RD0RD_1LE1RC_1RA1LE_1RE0LF |
STUCK (parked) | removed (equivalence) | Eqv_WordPairs.v TM83 makes it equivalent to 1LB---_1RC0RC_1LD1RB_1RE1LD_0RA1RF_1RD0LF, which stays. Nothing lost: it stays parked, and any future work targets that representative. |
| the 11 other kills (#3 #4 #11 #12 twin#12 #24 #25 #33 + 3 family-sweep relatives) | KILLED, not submitted | all present | unchanged; still count |
| everything else in machines/ (funded, parked, cryptid) | — | all present | unchanged |
What this means for next steps
- Submission gate is open. You said you would wait for a response to #2 before posting the next family. The response came: a merge within about 2 hours and no comments. Ready next, each a family that shares one proof idea:
- #3 + #24 + #25 +
1RB0RD_1RC1RF_…(4 machines, one table) - #11 + #33 +1RB0LD_1RC0RE_…(3) - #12 + its twin (2) - #4 +1RB---_0LC1RF_…(2)
My suggestion: #3's family next, as one PR with 4 files, since all four share one table and one proof. The PR text and Discord message would follow #2's format.
2. Switch our reference list to 740. Nothing pins it now: tools (dashboard.py, killreview.py, compress/rulefit) and workflow prompts still read 2026-10-07_778.txt, and the formalize audit checks membership against it. A kill on a machine removed by equivalence would no longer shrink the list, so new work should be gated on 740. (Tests can keep their 778 fixtures.)
3. Refresh solved_index / equivalence data. data/solved_index.tsv and 2026-10-07_eqv_1590.txt predate d3c52f5. Re-indexing against 9cf9e88 adds the 6 new files.
4. Record provenance. Add the 740 list to data/holdouts/SOURCES.md, naming its source (wiki upload or Discord) and date. The repo convention would name it YYYY-MM-DD_740.txt.