BB(6) community landscape for Track B targeting

Compiled 2026-10-09. Scope: the bbchallenge wiki (all 2026 monthly reports, TYBR 2025, BB(6), Holdouts lists, Cryptids, BMO, 103 per-machine pages, user pages), the annotated spreadsheet (12 CSV tabs, link and strikethrough sidecars, and xlsx comments), GitHub (busycoq PRs, 2026 community repos), the discuss.bbchallenge.org forum, and web search. Discord is the primary venue, and we cannot read it. Everything here is second-hand from wiki/TMBR summaries, sheet notes, and GitHub.

This complements the busycoq git-history forensics done in parallel and does not repeat it.

Caveat on sources: the TMBR pages for May to October 2026 are marked "in progress and has not yet been released" on the wiki and may still change. Jan to Apr 2026 are released.

0. TL;DR for Track B

1. The maintainer is the biggest AI user in BB(6). mxdys has used LLMs to write Rocq proofs since at least July 2026. - Aug 15: 20 machines (all of Counter Class 1 plus 4 Dekaheptoids), 32 more Rocq proofs, and decider settings for 10 others. - The fall in holdouts from 1,064 (Jul 28) to 778 (Oct 7) is largely his LLM-assisted proofs and new decider families. - Consequence: "easy" machines disappear fast. Anything that one of his decider families can absorb will probably be absorbed before we finish.
2. AI help is normal and openly disclosed. The bar is that the proof is checked, not who wrote it. - Rocq proofs that compile against BB6 are accepted whatever their origin. - Lean-only proofs, AI-made deciders, and informal AI claims are labelled "unofficial", "not independently verified", or "moderate rigor". They do not change the Rocq-verified count. - Wording seen on the wiki: "Note that the formal proofs were made with the help of Claude Opus and Aristotle AI"; "(Note that the new holdout lists are unofficial, as the correctness of the deciders has not yet been verified)".
3. Proofs are accepted through Discord, not PRs. - The pinned branch (ccz181078/busycoq, BB6) has 13 PRs in total. Two were merged: sligocki's Antihydra (2025) and univerz's "vibecoded" CounterRegular.v. CounterRegular.v was deleted the next day in mxdys's commit 605d26d ("add BMO9, S18, SOBCv11,v12"). - A Claude-written halting proof (JacobRSchwartz-AI, PR #2, the "Odometer") was closed within 5 hours: "with your hint, this TM was newly proven in verify/UBRRBAHaltv2.v". - 8 PRs from an AI agent (mira-quine) have had no response for 9 days. - The pattern: mxdys takes the insight and re-proves it in his own decider or family framework. A hint plus a short, readable argument is what actually moves the list.
4. Machines that are already claimed or have a proof pending (avoid, or coordinate first): - 21 machines in mira-quine's open PRs (§7.1); - 1RB0RA_0LC0LA_1RF1LD_1LE0LD_1LC1LF_---1RA, which has a public Lean 4 proof (M-Abozaid, Sep 28) that busycoq does not include; - dyuan's Oct 1 list of 24 machines that are "easy by longitudinal analysis" and mxdys's Aug 24 list of 86 machines that are "easy to accelerate with UBRRBA". Both are Discord-only; Dennis should fetch them.
5. Where the open machines are (my per-class count on the 778 list, which matches T English's sheet comments almost exactly; §5): - Shift-overflow counter 128, Skelet 1-like Class 1 101, Unknown 93, Bell-like 80, Quadratic Mess 51, Cubic Mess 50, Bell eats counter 40, SO bouncer counter 33, and so on. - SOC is the maintainer's active front (418 → 128 in 2026). - Classes nobody has touched in 2026 are either tarpits or neglected: Chaotic Bell Class 3 (22, 0 solved), Chaotic 1dCA-like in bell (9), Structural counter + counter (5), Counter Class 4 (2).
6. Tarpits to exclude from the pilot (§6): - the 20 cryptids and 7 potential cryptids; - the open BMO problems (1, 5, 6, 8, 10, 11); - the "Machines at the Edge" (tetrational or probviously-halting simulation lotteries); - most of Skelet 1-like Class 1.
7. Spreadsheet staleness: the Results tab covers the 1,534 list (Nov 2025). The Statistics tab itself says "Results outdated, Direct Sim up-to-date". Use it for notes and people, not for status. Status comes from the 778 list and its equivalence file.

1. The 2026 timeline (BB(6) only)

Holdout counts are mxdys's lists, counted up to equivalence. Dates are when the list was shared on Discord.

From Jul 28 to Oct 7 the list fell by 286 machines (27%) in 10 weeks. That is more than in the whole first half of the year.

Month by month (who killed what, and how)

Background in 2025 (TYBR: 2025): - mxdys's FAR with a DFA generator (Nov 2025) decided 113 of 1,534 on first run. - @Bricks published a block-analysis susceptibility score with a spreadsheet. - vonhust wrote a ~2×10⁹ steps/s bit-packed macro simulator. - Robin Rovenszky (RobinCodes) started the annotated spreadsheet on 2025-11-22. - mxdys found the champion (1RB1RA_1RC1RZ_1LD0RF_1RA0LE_0LD1RC_1RA0RE, > 10↑↑10↑↑10↑↑8) in June 2025.

January (1326 → 1314): - Simulation push: Alistaire and aparker simulated machines out to 10¹³, which turned up two halters for Alistaire: 1RB1LB_1LC0RC_1RE0LD_0RE0LA_1RA1RF_---1RC (~4.2e12 steps) and 1RB0RD_1LC1LD_1RD0LB_1LC0RE_0RF1RA_---1RC (~1.5e18). aparker finished the last "Unknown"-class machine. - Halters: Peacemaker II found two with a bespoke accelerated simulator. - Informal proofs: dyuan gave informal nonhalting proofs for two machines using longitudinal analysis. - mxdys: - posted a "seem provable" list (Discord forum thread 1460495597386731643, which the sheet's Next-Steps page also links); - released C++ FAR plus a DFA generator on Jan 18. This became the workhorse for Andrew Ducharme, prurq and Peacemaker; - started translating three halting proofs into Rocq, including one by Racheline from July 2024 that had been overlooked.

February (1314 → 1214; 100 solved): - Halters: prurq found one at 30,505,241,149,212 steps; mxdys found two more the same day (all three checked in C++). - Andrew Ducharme: 7 + 9 nonhalting machines with mxdys's C++ FAR. - Alistaire: 1 nonhalting machine with Quick_Sim.py. - mxdys: a new longitudinal-acceleration method, which was very productive. - Simulation: prurq's "Cascade" simulator, and by Mar 1 every holdout had been simulated to 10¹³ (prurq, Alistaire, mammillaria).

March (1214 → 1161): - Simulation lists: lists of machines not yet simulated to 10¹⁴ and 10¹⁵ were created (178 and 252 entries). - FAR: Ducharme 3 machines, mxdys 2. - Translated cyclers: prurq found 2, and Shawn Ligocki verified one with a preperiod above 10¹². mxdys found 4 more. - Cryptids: DrDisentangle showed 1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC to be a probviously nonhalting cryptid like Space Needle. - Tools: mxdys published the LongAcc web visualizer (https://ccz181078.github.io/TM/LongAcc/). - AI, BB-adjacent: Jason Yuen (@-d) used Claude Opus 4.6 to settle all 140 BBf(21) holdouts and found the Fenrir cryptid in BBf(22). The Cryptids page credits it to "Jason Yuen (@-d) and Claude Opus 4.6".

April (1161 → 1104): - Cryptids: sheep found a new cryptid, 1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE, like Space Needle, which Daniel Yuan showed to be a cryptid. A classification of cryptids into classes such as "Needles" began. BMO 8 was added. - Formalization: 1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB--- was formalized in Lean assuming the Baker–Wüstholz bound as an axiom. The repo is rwst/bbchallenge (DrDisentangle), "made with the help of Claude Opus and Aristotle AI". - Equivalences: most of the reduction came from new equivalences that -d helped find. -d estimates 100–200 equivalences remain. - AI, BB(2,5): mammillaria proved BMO 3 in Lean with Aristotle, and mxdys translated it into Rocq "using LLMs".

May: no BB(6) list. - mxdys made Inductive_inf.v (a history-linear inductive decider) compile into an executable. - David SG released GPU deciders (David5768/David-BB7-GPU-Deciders) and contributed some BB(6) results. The TMBR TODO to list them was never filled in.

June (1104 → 1094): - FAR: mxdys 4, prurq 4, and Peacemaker II 1 (with high parameters). - Proofs: hipparcos proved 2 machines nonhalting, and mxdys checked both in Rocq.

July (1094 → 1064): - mxdys: solved 5 in Rocq, one of them on Jul 3 "with the help of an LLM". This is the first BB(6) mention of the maintainer using an LLM. - Halters: prurq found one, which mxdys checked in Rocq. - AI, BB-adjacent: Marcelo Fornet finished BB(5) in Lean with Claude, and carrino reduced BBB(4) using Claude (§3.2).

August (1064 → 999): - BMO: mxdys added BMO 9 and 10. - Halters: - prurq simulated 4 machines to halting, one of them ~2.6e304 steps. He confirmed it with mxdys's LongAcc. - q64 proved 2 machines halting (Aug 4, Aug 26) in his fork Quantum64/busycoq. - jacobrschwartz proved the "Odometer" halts (Claude Fable 5; §3.1). - flintt_6 gave an informal halting proof (github golirt1/bb6-shift-overflow-analysis, now returns 404). - Aug 15: mxdys, "using an LLM", produced proofs for 20 machines (all of Counter Class 1 plus 4 Dekaheptoids): 2 confirmed, 18 under review. He also produced 32 other Rocq proofs and found decider configurations that settle 10 more. - Aug 24: mxdys posted a list of 86 machines that are easy to accelerate with the UBRRBA decider. - Cryptid definition debate: person89 and Shawn Ligocki argued over what counts as a cryptid and whether BMO1 is one. Shawn suggested cryptid-ness is a spectrum.

September (999 → 797): - Counter Class 1: mxdys solved all 16 by Sep 4. - New contributor: fifi_49513 claimed a nonhalting proof in a Discord thread on Sep 4, and mxdys confirmed it in Rocq on Sep 5. That is the normal path for a newcomer. - What the Sep 24 list (815) removed: BMO 9, 2 shift-overflow bell counters, 31 shift-overflow mixed-digit counters with similar behaviour, 2 high-period translated cyclers, and 2 other shift-overflow counters. - Space Needle: Seiji extended the trajectory to 10⁸ terms (oohzaim1-afk/space-needle-100M). - 1RB1LA_1RC1RE_…_0RB---: formalized without new axioms by avoiding Baker–Wüstholz. It is not on the 778 list (last seen on the 999 list). - PRs: - univerz's "vibecoded" CounterRegular.v was merged Sep 23 and deleted Sep 24. - zero-context opened PRs #3 and #4 on Sep 2 (an unsound Admitted; §4.4). - mira-quine has opened PRs since Sep 30. - Spreadsheet: RobinCodes began updating the sheet (Sep 2). T English annotated per-class remaining counts (Sep 16 to Oct 8).

October (797 → 778): - dyuan shared 24 holdouts expected to be easy by longitudinal analysis (Oct 1; Discord only). - mxdys released the 778 list (Oct 7).

Methods that killed BB(6) machines in 2026, roughly in order of volume

1. mxdys's decider families, versioned and extended week by week: SOC*/SOCSS, SOBC, BTC, SOTC, RRBA/UBRRBA, CubicCap, BLEC, Inductive, and others.
2. mxdys's C++ FAR with the DFA generator, run by Andrew Ducharme, prurq, Peacemaker II and mxdys himself.
3. Equivalence finding (Eqv_v2/v3; -d's help in April).
4. LLM-assisted individual Rocq proofs by mxdys (Jul to Sep).
5. Accelerated simulation to halting (prurq's Cascade, Quick_Sim, LongAcc, and bespoke simulators).
6. Translated-cycler detection with long preperiods.
7. Individual human proofs, most of them formalized by mxdys (hipparcos, dyuan, fifi_49513, Racheline, Peacemaker).

2. Who is active (BB(6) and nearby)

Takeaway: almost every new outside contributor in 2026 is using Claude or another LLM agent, so Dennis's approach is not unusual. The scarce resource is mxdys's review attention.

3. AI and LLM assistance: catalogue and reception

3.1 Inside BB(6)

3.2 Nearby domains (they set the norms)

• BB(5) in Lean (Marcelo Fornet with Claude, July): completed Jul 25 and reported as a milestone.
• BBB(4) = 32,779,478 (carrino with Claude, Aug 2): Coq repo, "one axiom". TMBR headlined it and made the August banner image for it. The Holdouts-lists page states it as solved. This is the most positive reception of an AI-heavy result.
• Fractran (-d with Claude Opus 4.6 and 4.8):
• BBf(21) is "tentatively" proved.
• The Fenrir cryptid is co-credited to Claude on the Cryptids page.
• The BBf(23) and BBf(24) holdout lists made with AI deciders are kept as "unofficial" and reported next to the official counts (e.g. "231,432 holdouts, or 10,838 if ai-created deciders are used").
• BB(2,5) (prurq with GPT-6 and Aristotle; 22 Lean proofs, Sep 25 to Oct 2):
• The wiki files them under "Solved with moderate rigor … however their proofs have not been independently verified".
• The Holdouts-lists row reads "22 proofs in Lean using GPT6 and Aristotle. To be independently verified".
• The official Rocq count stays at 60.
• BMO 3 (mammillaria with Aristotle in Lean, then mxdys translating to Rocq "using other LLM"): this was accepted, and the Rocq version is what counts.
• MBB(8) (register machines, Oct): -d and Shawn Ligocki publish both "after reduction" and "if an ai-created decider is used" counts.
• Twitter @Mira___Mira (GPT-6 Astra): claims of ZFC- and PA-independent machines are reported in TMBR as "claimed", pending a Metamath formalization.
• Elsewhere: BMO problems were added to DeepMind's formal-conjectures database (FormalConjectures/Other/BeaverMathOlympiad.lean), so AI-lab provers may target BMO 1, 5, 6, 8, 10 and 11.

3.3 Reading of community norms on AI

• Disclosure is the norm and costs nothing: "Co-Authored-By: Claude …" trailers, wiki headings such as "Analysis by Opus 4.7 / DrDisentangle", and TMBR notes such as "made with the help of …". I found no hostility to disclosed AI use on any page.
• Verification is what matters. A result counts toward the Rocq-verified count only once it is in busycoq's BB6 branch, in practice through mxdys. Lean proofs and AI-written deciders get a separate "unofficial" or "to be independently verified" label.
• Volume does not equal acceptance. Large, generated, multi-file PRs (mira-quine, zero-context, and to a lesser extent the Odometer) get either silence or "thanks, I re-proved it in my framework". The maintainer clearly prefers to fold results into his versioned family files over merging bespoke proof developments.
• Readable informal arguments are valued: rule tables, BMO-style reformulations, "why it can't halt" sections. Both TMBR and the wiki surface who explained the behaviour, not only who produced a .v file.
• No explicitly AI-attributed incorrect proof was found in the sheet or on the wiki. The sheet tab "Unverified probably incorrect proofs" (§4.3) holds 6 human-attributed claims and says nothing about AI. One LLM-flavoured crank post on the forum ("Antihydra copycat", Mar 2026) got a patient, polite correction from aparker.

4. How proofs get accepted (submission norms)

4.1 The actual pipeline

1. Discuss on Discord. Use the #bb6 channel (1239205785913790465) or a dedicated thread per machine. sligocki on the forum (Sep 2026): "The bulk of the discussion is happening on our Discord server … there is a dedicated #bb6 channel".
2. mxdys formalizes or verifies. This is often the same day: hipparcos in June; fifi_49513 on Sep 4 to Sep 5; prurq's halters; "confirmed in Rocq by mxdys".
3. The proof lands in the busycoq BB6 branch as mxdys's commit, usually in one of his family files.
4. The next holdout list drops the machine. TMBR records who did what. RobinCodes updates the sheet when he has time.

4.2 PRs to ccz181078/busycoq (all 13 ever)

Issues are disabled on the repo.

For our submissions: - Post on Discord first, in a per-machine thread, with: - the TM string; - a short rule table and why it never halts (or halts); - a single-file .v in house style (§4.3); - the check_kill output; - a one-line AI disclosure. - Offer a PR only if mxdys asks for one. Batches of small files will be easier to absorb than a 15-file development.

4.3 What "house style" means, from the busycoq README and the merged code

• Use the existing framework. Proofs are individual .v files in verify/ built on Individual62, with TM_from_str, es/follow/ind, and multistep_nonhalt plus progress_nonhalt_*. Equivalences go through Eqv_v2 or Eqv_v3.
• "Don't refactor anything" (README). The ~3,000 individual proofs and the decider pipeline are not compiled by make ("about a month").
• Two methods the README endorses:
• a proof template: a parameterized proof plus a parameter search;
• "copy and modify existing proofs".
• Comment blocks with the human-readable rule tables at the bottom of each file. Some of mxdys's 2026 files say "generated", e.g. QuadraticMess30.v: "The entire route is generated by a proved RLE parameter interpreter."

4.4 Relevant to our check_kill.sh

zero-context's PR #3 shows the BB6 branch contains unsound Admitted lemmas: - BBinf.all_qs_spec and all_syms_spec are provably False. - Similar admits sit in TMLR.v, TMAddOneSymbol.v and TMLocalHistory.v. - They are registered with #[export] Hint Resolve … : core, so a bare auto could silently use False.

Our gate already guards against this: Print Assumptions must match the baseline {functional_extensionality_dep}. Still, our proofs must not Require BBinf, TMLR, TMAddOneSymbol, TMLocalHistory or Inductive_inf. It would be worth adding a check that greps for those imports.

4.5 Counting conventions (Statistics tab)

• Informal count: includes informally solved machines.
• Formal count: "produced by highly trusted code or reproduced, or shared in a formal format and overseen by others, but not Rocq-verified".
• Rocq-verified count.
• The tab's own numbers (998/999/999) are stale. Our kills should aim at the Rocq-verified count.

5. The annotated spreadsheet

Snapshot of 2026-10-09: 12 tabs, plus our _links.csv (749 hyperlinks, mostly Discord), _strikethrough.csv (627 struck cells, meaning done), and the xlsx comments. Hungarian locale: "Megjelölve lezártként" means "marked as resolved" and "Újra megnyitva" means "reopened".

5.1 What each tab means

5.2 Cell comments (xlsx)

T English, Statistics tab (Sep 16 to Oct 8): 30 comments, each giving the current remaining count next to a class's old count. I recomputed the per-class counts on the 778 list and they match exactly except Counter Class 3 (comment says 4, now 3). For example: - SO bouncer counter 42→33 - Chaotic Bell Class 3 22→22 - Spaghetti 21→18 - Skelet 1-like Class 2 15→14 - Counter Class 1 16→0 - Skelet 17-like 8→0

The comments skip the big classes (SOC, Skelet-1-like Class 1, Bell-like, Cubic/Quadratic Mess, Bell eats counter, Unknown), so T English is evidently partway through a Statistics refresh.

Direct Simulation tab: - Gabriel Whigham simulated several machines: one to 2.33e13, one to 1.17e14. On 1RB1RE_1LC1RC_0RF1LD_1LE0LB_1LB0RA_---1RA his computer crashed at ~40% and he wrote "This is back up for grabs" (Feb 27). - Avery Parker: 1RB0LF_1LC1RF_---1LD_0LE0LB_0RA0LA_0RA1RB was simulated to 1.7e15 with "some sort of change in behavior somewhere after 2.7e13 steps". - Albert Kościelniak, Apr 3: "Claiming this group for now." This is Group 21 of the 10¹⁴ list. 3 of its 5 machines are struck. The 2 still pending are 1RB0RF_0LC0RD_1LD1LC_1RE1LB_---1RA_0LF0RC and 1RB0RF_0LC1LB_1RD1LA_1RE0LC_0RA1RD_---0RC. The claim may be stale.

Results and Archive tabs (Alis Anon): a link to the ">1e15" Discord thread, and Dec 2025 "running" notes.

5.3 Notes mined for open machines (Results, Level 0/1, Discarded): difficulty, partial progress, claims

Probviously and cryptid suspicions (all still open): - Racheline: - "Probviously halts after 10^10^O(1) steps, possibly tetrational" on 1RB1RF_1LC0RA_---0LD_0LE0LB_1RF1RB_1RE1LF, which has since been solved; - "Possibly tetrational machine" on 1RB1RD_1LC1RA_---1LD_1LE0RA_1LF0LE_0RB0LB, 1RB0LE_0RC0RA_1LD0LC_1LA0LB_1RA1LF_---0LC and 1RB1LE_0LC1RE_---1LD_0RD1LA_0RF1RF_1RA0LB; - "Potential cryptid (if so, probviously nonhalting)" on 1RB1RF_1LC1LF_0RE1LD_0LB1LD_---1RC_1RA0RD; - "Collatz-like" on 1RB1RA_1LC0RC_---0LD_0LE0RF_1RE0RA_0LF1LB; - "No clear path to halting yet" on 1RB1RA_1LC1LE_0LD0LB_0RA0RF_0LC0RA_1RD---; - "Probably doesnt halt" on 1RB0RC_1LC1RA_0RF0LD_1LE0RB_1LB0LD_---1RD. - Others: "Probviously halting machine" (Peacemaker, Legion, hipparcos, dyuan) on 1RB0LA_0RC0RB_1LD1LA_1LC1RE_1RF0RD_1LC---, which is also on Machines at the Edge as "around a day with 100–1000 GB"; dyuan's "Similar to BMO 1?" on 1RB1RD_0LC1RA_0RA1LC_1RA1LE_1RF0LD_---0RE; "Very strange machine" (-d) on 1RB1LE_1LC0RA_0RF0LD_1LE1LA_1RC0LB_---1RC.

Partial progress or simulation depth (Alistaire unless noted): - 1.03e73975 steps: 1RB1LC_1LA1RF_0RD1RD_0RA0LE_1LA0LE_0RC--- - 9.41e160394 steps: 1RB1LF_0LC0RE_1LA1RD_0LB1LB_1RC1RD_0LD--- - 1e2848 steps: 1RB---_1RC1LE_0RD0RF_0RE0LA_1LF0LB_1LA1LD - 10^190,000 steps (Polygon, hipparcos): 1RB1LE_1LB1LC_1RD0LE_---0RB_1RF1LA_0RA0RD - 10^4600 steps, "code with log reduction" (nerdyjoe): 1RB1RF_1LC1RD_1LA1LC_1RA0RE_1RD1LA_---0LE - "Ran until sigma of 10^97" (Ducharme): 1RB0LB_0LC0RE_1LA1LD_0LB1LF_1RA1RD_0LB--- - "Partial analysis, simulated up to 2.3e14" (yourself, Atoms, hipparcos): 1RB0LC_1RC1RA_1RD0RF_0LE---_1LA1LE_0RA1RF - "Analysis. Conjecture: Nonhalt. Simulated to 1e16.3" (nerdyjoe, Alistaire): 1RB0RB_1RC0LE_1LD1LA_---0LC_1RF1LE_1RA0RA - "~10^64 tape size and doesn't halt or become a TC yet" (mxdys): 1RB0LC_0RC1RF_1RD0RE_1LE0RA_0LA0LE_1RE--- - "Strange ternary counter" (hipparcos): 1RB0LC_1LA0RD_1RA0LA_1RE1RD_1RA1RF_1LC---

Machines whose notes say they may be easy (all open; check Discord before touching): - "Appears to be solvable" / "Looks like a solvable fractal": 1RB1LE_0RC1RC_0RD0RB_1RE0RF_1LA0LE_---1RB (Chaotic Fractal Type 1) - "Could be solvable" / "Seems easy" (Katelyn Doucette): 1RB1RD_1LC0LE_1RA0LB_1RA1RF_0RA0RC_1RE--- (Bell-like) - "Should be CTL-able" (Legion): 1RB---_0RC1RD_1LD1LF_1LE0RB_1RF1LD_1LA0LC and 1RB1LB_1LC0RD_0LE1LA_0RF1RA_1LE0LA_---0RB (both Chaotic 1dCA-like in bouncer) - "Possible bouncer with high params": 1RB---_1LC0RF_1RF0LD_0LE1LC_0RC0LC_1RB0RA (Unknown) and the group led by 1RB---_1LC0RF… - "Possible bouncer": 1RB0LB_0LC0RE_1LA1LD_0LB1LD_1RA0RF_1RA--- (Chaotic Bell Class 4) - "Has to halt in the counting phase" / "Looks TC": 1RB0LA_1RC---_0LD1RD_0RA0RE_0RF1RC_1LF0LA (Translated Counter; also "the machine with the least common transitions") - The 2025 "should be solvable / easy" list on User:RobinCodes/Next Steps (22 machines with low visited-cell counts, ≤ 68 cells in 10⁹ steps) has been mostly cleared. Rerun it against the 778 list before using it.

Difficulty quotes from the Discarded tab: - "shift overflow counter seems hard - mxdys" on 1RB0RF_1LC1RE_0LD0LC_1RD0RB_1RA0RB_1RC--- - "Looks like hell - Katelyn Doucette" on 1RB0RD_1LC1LB_---1LD_1RA0RE_1RD0LF_1LE0LD - "In a class of ~30 similar holdouts - mxdys" on 1RB1RD_1LC0RE_1LD1LC_1RA0LE_1LC0RF_0RD--- (Chaotic Bell Class 1) - "Racheline mentions starting a proof but never shares" on 1RB0RE_1LC0RA_1RF0RD_---1LE_0LB1LE_1LE1RC: a possible stale claim - "Peacemaker asked someone to run something on it, wasn't done" on 1RB1RA_1LC0RB_1LD0LB_1RA0LE_---1LF_1LB0LA - 18 entries noted as "It's equivalent machine was solved erroneously in BB7 :)" (shift-overflow counters). These are a warning that BB(7)-pipeline results for SOCs had at least one false positive.

Sheet anomaly (already in STATUS.md): Results row 232 marks 1RB1LC_0RC0RB_1LD0LA_1LE---_1LF1RA_1LA1LC as NONHALT "SOCSSv5.v (March 2026)", but it is still a 778 representative.

5.4 "Unverified probably incorrect proofs" tab

• Edward_Z: SOC; the machine is now closed.
• nerdyjoe ×3:
• "Should be CTL-able (NONHALT is unverified result and unlikely to be correct)": 1RB1LB_1LC0RD_0LE1LA_0RF1RA_1LE0LA_---0RB, open;
• 1RB0RE_1LC0RA_0LD0LB_1RE0LB_1RF---_0RB0RC, open;
• "Via a method akin to backwards-reasoning": 1RB1RB_0LC0LD_0LE1LD_1LB0RE_1RA0RF_1RD---, open.
• Mino: closed.
• vonhust: "HALT (?) Informal, unverified result (unlikely to be correct)" on 1RB0RE_0RC---_1LD1LE_1LE1LD_1RF0LC_1RA1RF, which is open (Chaotic 1dCA-like in bell).

No AI attribution on any of them. These 4 open machines are known traps: a wrong argument has already been made for each.

6. Class landscape and tarpits

6.1 Per-class drain across 2026 (classified by membership, from the 1326, 1064 and 778 lists)

How to read the table: - Active maintainer fronts, where duplicate risk is high: - shift-overflow counters (new SOC/SOBC/SOTC/BTC/mixed-digit families every week); - Chaotic Fractal Type 1 (22 → 4 in 10 weeks); - Monotone list; - Sync bouncer counter. - Medium: Cubic and Quadratic Mess, Bell eats counter, SO bouncer counter. - Stalled: Chaotic Bell Class 3, Chaotic 1dCA-like in bell, Structural counter + counter, Counter Class 4, Skelet 1-like Classes 1 and 2, Chaotic Ack-like Bell. These are either genuinely hard or nobody has tried them. Chaotic Bell Class 3 is interesting: 9 of its siblings fell to FAR, so it may need FAR with stronger DFA parameters, or a counting argument over "two arrays of integers". - "Unknown" (93): largely unanalysed. Most have no notes at all beyond simulation depth. This is where new structure might be found, but also where the true monsters may hide.

6.2 Known tarpits: exclude from the pilot

All of these are confirmed open on the 778 list. - Probviously nonhalting cryptids (9): - Antihydra 1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA; - 1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA; - 1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC; - 1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---; - 1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB; - Space Needle (BMO 6) 1RB1LA_1LC0RE_1LF1LD_0RB0LA_1RC1RE_---0LD; - SN-like 1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC, 1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE and 1RB0RF_1RC1RF_1LD0LE_---1LC_1RA1LE_1LC1RB. - Probviously halting cryptids (10, plus 1 that is 3/5 TC and 2/5 halt): - Lucy's Moonlight 1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA; - 1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC, whose 16-machine family is one equivalence group of 16; - 1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF; - 1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB; - 1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA; - 1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE; - 1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA; - 1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE; - 1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB; - 1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LE---; - 1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE (the 3/5 TC, 2/5 halt case). - Potential cryptids and open BMO problems: - BMO 1 1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE; - BMO 5 1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE, plus its "start from D/C" variants 1RB1RE_1LC0RA_1RD0LB_1LB1RC_1LF0RD_---0LE and 1RB1LC_1RC0LD_1LA0RB_1LB1LE_1RF0LA_---0RE; - BMO 8 1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA and BMO8-like 1RB---_0RC0RD_1LD1RB_0LE0LC_1RA0LF_1LD1LE; - BMO 10 1RB0LB_0RC0LD_1LD1RE_0LA0RF_0RD1RF_0RC--- (a group of 4); - BMO 11 1RB0LD_0LC0RE_1LA0RD_0RB0LC_1RC1RF_0LD---, a member of the group of 20 led by 1RB0LD_0RC---_1LD0RF_0LE0RA_0RA1LF_0LA1LB. This makes the whole 20-machine SOC group a tarpit. - 1RB1RF_1LC1LF_0RE1LD_0LB1LD_---1RC_1RA0RD, 1RB1RF_0LC0RF_1RD1LC_---0LE_0RC1LF_1RA0LE, and the 2-undefined-transition 1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF (group of 9; DrDisentangle and Opus could not close the C,1 halt condition). - Machines at the Edge (User:RobinCodes): simulation lotteries, not proofs. - 1RB0LA_0RC0RB_1LD1LA_1LC1RE_1RF0RD_1LC---: "around a day with 100–1000 GB". - "Possibly tetrational": 1RB1LE_0LC1RE_---1LD_0RD1LA_0RF1RF_1RA0LB (group of 6), 1RB1RD_1LC1RA_---1LD_1LE0RA_1LF0LE_0RB0LB and 1RB0LE_0RC0RA_1LD0LC_1LA0LB_1RA1LF_---0LC. - The other two "holdouts with 2 undefined transitions" (SOC): 1RB---_1RC---_1RD1LC_1LE1RF_1LC0LE_1RA0RD and 1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LF---_1LC---. - Discarded-tab "hell" and "seems hard" quotes (§5.3) and the 4 open "probably incorrect proof" machines (§5.4).

7. What is claimed or in flight (as of 2026-10-09)

7.1 Open busycoq PRs by mira-quine (AI agent, OpenAI-assisted; unmerged, all still representatives on 778)

• #6: 1RB1LC_1LC0RD_0LE1LA_0RF1RA_1RD0LA_---0RB ≡ 1RB1LC_1LC0RD_0LE1LA_---1RA_1RF0LA_0RF0RB
• #7: 1RB1RE_0LC1RF_---1LD_1LE0LD_1LA1LB_1RE0RA ≡ 1RB1RE_0LC1RF_---1LD_1LE0LD_1LA1LB_1RF0RA
• #8:
• 1RB0LC_1LA1RF_1LD1RF_1LE0LA_0RB---_0RA1RE ≡ 1RB0LC_1LA1RE_1LD1RE_1RE0LA_0RA1RF_0RB---
• 1RB1LF_1LC1RE_1LD1RD_1LA0LB_0RC---_1RC0LD ≡ 1RB1LE_0RC1RF_1LD1RD_1LA0LB_1RC0LD_0RC---
• 1RB1LE_1RC0RF_0LD---_1RF1LE_0LF1LC_1LD0RA ≡ 1RB1LC_1LC0RF_0LF1LD_0LE---_1RF1LC_1LE0RA
• 1RB0RF_0RC1RD_0LD---_1LE1RA_1LA0LF_0RD0RC ≡ 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
• #9: 1RB0RC_1LC0RB_1RE1LD_0LB0LF_---0RA_1LB0RC ≡ 1RB0RC_1LC0RB_1RE1LD_0LB0LF_---0RA_1LB1LD
• #10: 1RB1LC_1LA0RD_0LB1LF_1RE1LC_1LC0RB_0LA--- ≡ 1RB0RE_0LC---_1RE1LD_0LE1LB_1LC0RF_1RA1LD
• #11: 1RB0LE_0RC1RC_0RD1LA_1LD0LA_1LF1LC_---1LC ≡ 1RB0LE_0RC1RC_0RD1LA_1LD0LA_1LF1LC_---0LA
• #12: 1RB1LD_0RC1LE_1RD0LA_1RE0RC_1LF0LC_---1LB ≡ 1RB1LD_0RC1LE_1RD0LA_1RE0RF_1LF0LC_---1LB
• #13 (nonhalt): 1RB0LA_0RC1LE_0RD1RE_1LA1RF_1RB0LD_1RC--- (row 9 of the 815 list)

The equivalences don't kill anything on their own: each merges two representatives into one. Still, any kill on one side of a pair kills both. That makes these pairs attractive if the claimed equivalence is right, and pointless to duplicate if someone is about to merge it. Note that #8's first pair includes 1RB0LC_1LA1RE_1LD1RE… and 1RB0LC_1LA1RF…, which nerdyjoe had already analysed (Level 1).

7.2 Other claims and lists that matter

• Public Lean proof not in busycoq: 1RB0RA_0LC0LA_1RF1LD_1LE0LD_1LC1LF_---1RA (M-Abozaid). A Rocq port would be a cheap kill if nobody else is doing it. Ask first.
• dyuan, Oct 1: 24 holdouts expected to be easy by longitudinal analysis (Discord message 1555244959840337973). dyuan or mxdys is likely to work through them.
• mxdys, Aug 24: 86 machines that are easy to accelerate with UBRRBA (message 1541486462330085496). These are probably being turned into UBRRBAv files.
• mxdys, Jan: "seem provable" forum thread (1460495597386731643).
• DrDisentangle: a formal-proof-stage tracker for every cryptid and potential cryptid (User:DrDisentangle/BB6 formal proofs). He is working on rule formalization in Lean, not on kills.
• Sheet: Racheline "started a proof" of 1RB0RE_1LC0RA_1RF0RD_---1LE_0LB1LE_1LE1RC. Albert claimed 10¹⁴ simulation Group 21 (Apr). T English and RobinCodes are refreshing the sheet.
• -d: estimated 100–200 equivalences left (Apr), and mira-quine is now mining them with an agent. Equivalence hunting is crowded.

8. Implications for Track B targeting

1. Choose targets mxdys's families will not absorb soon. Avoid SOC, SO-bouncer, SO-structural, Sync-bouncer and Monotone-list machines unless Checkpoint A finds something genuinely new. He opens a new family file for those almost weekly.
2. Promising, quieter classes for a pilot of 5 or more classes: - Chaotic Bell Class 2 (7) and Class 4 (5, including "possible bouncer"); - Translated Counter (5, including "has to halt in the counting phase"); - Counter Class 2, 3 and 4 (3, 3, 2), whose siblings fell with LLM help in Aug and Sep, so templates exist in verify/CounterClass*; - Structural counter + counter (5) and Structural counter + chaotic edge (11); - Fractal in Bouncer (3) and Chaotic Fractal Others (4); - a few "Unknown" machines that have notes, e.g. "Possible bouncer with high params" and "Code. Binary counting + bouncing" (nerdyjoe). - Use Level 0 notes as hints.
3. Before each machine: - make sure it is not in §6.2 or §7; - check the Results, Level 0/1 and Discarded notes (tools/holdouts.py lookup --sheet); - make sure it is not in dyuan's 24 or mxdys's 86 (Dennis has to fetch those).
4. Submission format that fits the norms: - a Discord thread per machine (or one per small batch); - a readable rule table and argument; - a single .v in house style that compiles against the pinned BB6 commit, with no import of the unsound-admit modules; - the check_kill log; - a one-line disclosure ("Found and formalized with Claude Code; reviewed by Dennis"). - Expect mxdys to re-prove or fold it into a family. Credit tends to follow the insight in TMBR either way.
5. Do not open large multi-file PRs. The 13-PR record shows they stall or get superseded.

9. Open questions for Dennis to check on Discord

1. Preferred format. Does mxdys want individual .v files posted in a thread, a PR, or just the argument? Does he mind LLM-written Rocq if it is short and readable? (He uses LLMs himself.) Is there a per-machine thread convention for BB(6) kills?
2. dyuan's 24 longitudinal-analysis machines (Oct 1, message 1555244959840337973). Get the list. Is anyone working through it?
3. mxdys's 86 UBRRBA machines (Aug 24, 1541486462330085496). Get the list. Which are left on 778, and is he processing them?
4. The mira-quine PRs (#6–#13). Will mxdys review them? Is there a community stance on unattended AI-agent PRs? The pairs in §7.1 are untouchable until this is answered.
5. 1RB0RA_0LC0LA_1RF1LD_1LE0LD_1LC1LF_---1RA. Is anyone porting M-Abozaid's Lean proof to Rocq? If not, it is a cheap pilot kill, with permission and credit.
6. zero-context's Admitted finding (PR #3/#4). Is mxdys aware? Does he want it fixed? This is relevant to trusting decider-backed results.
7. Stale claims. Is Racheline's proof of 1RB0RE_1LC0RA_1RF0RD_---1LE_0LB1LE_1LE1RC still in progress? Is Albert's 10¹⁴ Group 21 claim still active?
8. Sheet anomaly. 1RB1LC_0RC0RB_1LD0LA_1LE---_1LF1RA_1LA1LC: the Results tab says NONHALT via SOCSSv5.v, but it is still on 778. Is that a sheet error or a missing equivalence?
9. The "solved erroneously in BB7" note on 18 SOC-equivalent machines. Which BB(7) decider produced the false positive, and is it fixed? This affects how much we trust any decider output we reuse.
10. Chaotic Bell Class 3 (22 open, 0 kills in 2026). Has anyone tried stronger FAR or DFA parameters since Katelyn's 9? Is it considered hopeless?
11. Is there a current "who is working on what" list for BB(6) (pinned message or thread), beyond the sheet? Is the April -d/mxdys equivalence push finished?
12. Status of David SG's GPU-decider BB(6) results (May): which machines? The TMBR TODO was never filled in.

Appendix: sources

Wiki (raw wikitext was pulled through the MediaWiki API on 2026-10-09; 103 per-machine BB(6) pages were also read): - Reports: TYBR: 2025 and TMBR Jan · Feb · Mar · Apr · May · Jun · Jul · Aug · Sep · Oct 2026 - Domain and topic pages: BB(6) · Holdouts lists · Cryptids · Beaver Math Olympiad · Probviously · Code repositories · BB(2,5) - User pages: User:DrDisentangle/BB6 formal proofs · User:RobinCodes/Next Steps · User:RobinCodes/Machines at the Edge - Machine page: 1RB1LA_1RC1RE_1LD0RB_1LA0LC_0RF0RD_0RB---

Spreadsheet: data/sheet/2026-10-09_*.csv, _links.csv, _strikethrough.csv, and the xlsx (comments1–4.xml, threadedComments1–4.xml, persons.xml). Machine status was recomputed against data/holdouts/2026-10-07_778.txt and 2026-10-07_eqv_1590.txt.

GitHub: - busycoq PRs #1–#13 (especially #2, #3, #4, #5, #6, #13) - Proof and analysis repos: JacobRSchwartz-AI/bb6-holdouts · M-Abozaid/bb6-nonhalt-1RB0RA_0LC0LA (and the two sibling repos) · rwst/bbchallenge · Quantum64/busycoq - Other 2026 repos: carrino/Coq-BBB4 · jeff87654/busy-beaver · rozetyp/bbrev6-settlement · oohzaim1-afk/space-needle-100M · mfornet/antihydra-autoresearch · David5768/David-BB7-GPU-Deciders · int-y1/BBFractran - AI co-authorship was taken from commit trailers.

Forum and blogs: - discuss.bbchallenge.org: "Where is the discussion of bb(6) candidates?" · "More Antihydra analysis" · "Antihydra Copycat" - Nick Drozd, "AI Reproduction of Lin's Busy Beaver Proof" (Jan 2026) - General web search for 2026 AI busy-beaver news turned up little beyond these. The wiki, GitHub and TMBR are the substantive record.