tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.The most recent overnight report: the kills and where each one stands upstream, the other machines, and what needs you.
insideKills: 31, each with tools/check_kill.sh PASS three times · Other machines · Halting hunt (10-13): no halt · Astra's audit of the 22 unmerged kills · 10-14 so far · What needs Dennis +1 more
reports/overnight-2026-10-10.md · 3 KB · updated Oct 14 18:03 · raw · ⤓
How every kill was proved: the common recipe, a table of the kills, what is special about each kind of proof, and one-breath summaries to use in chat.
inside1. The common recipe · 2. The 18 kills · 3. What is special about each kind of proof · 4. How to say it in one breath
reports/how-proved.md · 15 KB · updated Oct 13 15:48 · raw · ⤓
A wave's ranked picks: why each target, its nearest template, the risk, and the family the same proof covers.
insideWhat Wave 5 taught · Universe and checks · Picks · First step per pick, with stop rules · Launch order and resources · Notable rejections +3 more
reports/wave6/ranking.md · 31 KB · updated Oct 14 13:48 · raw · ⤓
A wave's ranked picks: why each target, its nearest template, the risk, and the family the same proof covers.
insideThe lesson from Wave 4 · Picks · First step per pick · Corrections to the scouts · Notable rejections · Critic (2026-10-13) +1 more
reports/wave5/ranking.md · 23 KB · updated Oct 13 00:51 · raw · ⤓
A wave's ranked picks: why each target, its nearest template, the risk, and the family the same proof covers.
insidePicks · Action outside the universe (worth more than most picks) · Notable rejections · Exclusions applied · Resource notes for the attack · Critic (completeness pass, 2026-10-10)
reports/wave4/ranking.md · 21 KB · updated Oct 10 23:15 · raw · ⤓
The BB(6) community around us: the 2026 timeline, who is active, how AI-assisted proofs are received, the submission norms, and what is claimed or in flight.
inside0. TL;DR for Track B · 1. The 2026 timeline (BB(6) only) · 2. Who is active (BB(6) and nearby) · 3. AI and LLM assistance: catalogue and reception · 4. How proofs get accepted (submission norms) · 5. The annotated spreadsheet +5 more
reports/landscape.md · 51 KB · updated Oct 9 21:48 · raw · ⤓
Which holdouts to attack and why: what gets absorbed fast, what is picked clean, the reusable templates, and our ranked candidate pool (#1, #2, …).
inside1. Executive summary · 2. The map · 3. Reusable proof templates and techniques per target class · 4. Candidate pool for the 20-machine pilot · 5. Questions for Dennis · Appendix: method notes and reproduction +1 more
reports/targeting.md · 47 KB · updated Oct 10 00:05 · raw · ⤓
Where the project stands: the pins, each phase, the open questions and every machine's line. Updated at the end of each session.
inside2026-10-16T12:14:18-07:00: W6-1 submitted as PR #29 · Sustained kill campaign active — 2026-10-16T09:37:53.088539-07:00 · Three-direction execution complete — 2026-10-15T20:10:45-07:00 · New research leads — 2026-10-15T18:37:12-07:00 · Eight proofs submitted — 2026-10-15T15:51:23-07:00 · New open competing submissions — 2026-10-15 15:15 PDT +6 more
The development plan: the mission, the ground rules, the phases and their gates, and the risks.
inside1. Mission · 2. Background (for a fresh session) · 3. Ground rules · 4. Workspace layout · 5. Phase 0: Setup (1–3 days) · 6. Phase 1: Atlas + pilot (~2 weeks, two parallel tracks) +7 more
2026-10-14, Wave 7 planner, then the adversarial critic pass (section "Critic" at the end). Built from the three lens tables in reports/wave7/ (lens-clusters.tsv, lens-triage.tsv, lens-unknown.tsv)…
reports/wave7/plan.md · 24 KB · updated Oct 14 19:52 · raw · ⤓
2026-10-14. Background: study.md in this folder. Lines 23, 206, 403, 415 (T1), 69, 245, 330, 668, 696 (T2), 178, 376, 382 (T3).
reports/cb3/decision.md · 8 KB · updated Oct 14 19:32 · raw · ⤓
Direction 4, option A (Dennis, 2026-10-14). Stages 1-2 of at most 3 done; stage 2 hit the stop rule (see the stage 2 log below). Option A is stopped until Dennis picks the next step (decision.md…
reports/cb3/explorer.md · 16 KB · updated Oct 14 19:30 · raw · ⤓
This is an independent check of coord/attempts.tsv. I did not rely on the backfill reports. I found each attempt in the original records and then looked it up in the ledger.
reports/attempts-coverage.md · 5 KB · updated Oct 14 19:03 · raw · ⤓
Goal: as much autonomous progress as possible, with nothing posted or pushed anywhere. Checkpoints are non-blocking (PLAN rule 9). Only check_kill.sh PASS counts as a kill.
reports/overnight-plan-2026-10-10.md · 7 KB · updated Oct 14 18:34 · raw · ⤓
2026-10-14. Background: atlas.md in this folder; stage 2 is its last section. K42 has no machine folder, so this card lives here.
reports/k42/decision.md · 5 KB · updated Oct 14 18:23 · raw · ⤓
2026-10-14. This merges five strategy lenses: census, verified deciders, family proofs, equivalence twins and cryptids. Paths are relative to [local working file] Numbers marked "est."…
reports/strategy/directions.md · 28 KB · updated Oct 14 18:03 · raw · ⤓
Stage 2 result (last section): with mxdys's 5^k acceleration, exact on all 40 lines, every line ran to 10^169-10^194 Incs with no halt and no translated cycle. Verdict: a cryptid family. The rules…
reports/k42/atlas.md · 54 KB · updated Oct 14 17:24 · raw · ⤓
We ported mxdys's 5^k-Inc acceleration (RIncs from Sk1like_TC_v2.v) to Python and made it exact for all 16 variants: anything the shared core table does not cover is handed to the real machine.
reports/k42/atlas_stage2.md · 22 KB · updated Oct 14 17:24 · raw · ⤓
Stage 2 result (last section): with mxdys's 5^k acceleration, exact on all 40 lines, every line ran to 10^169-10^194 Incs with no halt and no translated cycle. Verdict: a cryptid family. The rules…
reports/k42/atlas_head.md · 7 KB · updated Oct 14 17:24 · raw · ⤓
reports/k42/runs2/table.md · 7 KB · updated Oct 14 17:10 · raw · ⤓
Every variant has its own rule for an escape with a positive exponent m after the 01. It applies in all three F contexts (01^m, 00101^0 00101^m, 0011101^m) and also when the context is reached by…
reports/k42/atlas_qa.md · 11 KB · updated Oct 14 16:42 · raw · ⤓
2026-10-14, strategy direction 4. Claim: CB3 core (coord/claims.tsv). All paths are under [local working file]
reports/cb3/study.md · 14 KB · updated Oct 14 16:30 · raw · ⤓
reports/cb3/summary_table.md · 1,010 B · updated Oct 14 16:29 · raw · ⤓
Dennis (2026-10-14): apply Astra's patches. Source: coord/patches/astra-audit-public/ (17 patch files, READMEs, validation JSON). All target machines are Claude-owned (coord/claims.tsv, latest line…
reports/astra-patches-2026-10-14.md · 26 KB · updated Oct 14 10:21 · raw · ⤓
None of the four scouts (deep, margins, parked, hints) saw an in-scope machine halt. So no pick has a halt to replay; nothing here is a kill. Only tools/check_kill.sh --halt PASS counts.
reports/halting-hunt/ranking.md · 22 KB · updated Oct 13 19:17 · raw · ⤓
This ranks the untouched Bell eats counter machines on the 740 list for an attack now. The per-machine data is in reports/bec-sweep/universe.tsv.
reports/bec-sweep/ranking.md · 20 KB · updated Oct 13 16:00 · raw · ⤓
Open: /busy-beaver/dashboard/machines.html (click a tile to open its card). The server is running now. If it is down, restart it with: python3 -m http.server 8765 --bind 127.0.0.1…
reports/checkpoint-A-batch1.md · 14 KB · updated Oct 13 15:48 · raw · ⤓
Goal (Dennis, 2026-10-13): one simple, intuitive site. One nav, one page per machine, one machines table. Old URLs may break. The CLI commands keep their arguments. No information is lost: it moves.
reports/site-redesign.md · 36 KB · updated Oct 13 14:25 · raw · ⤓
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…
reports/holdouts-740-impact.md · 4 KB · updated Oct 10 15:47 · raw · ⤓
2026-10-10. Inputs: data/holdouts/2026-10-07_778.txt (778 entries), data/holdouts/2026-10-07_eqv_1590.txt (778 groups, 1,590 machines), the 9 machines/*/status.json with KILLED_NONHALT (#2, #3, #4…
reports/family-sweep.md · 30 KB · updated Oct 10 12:01 · raw · ⤓
2026-10-10. Not posted. Paste each block as one message. Both are under Discord's 2,000-character limit. The messages say "we"; add the disclosure line (targeting.md §5 Q8) if you want it.
reports/discord-drafts.md · 5 KB · updated Oct 10 09:32 · raw · ⤓
2026-10-09. busycoq BB6 @ 0940bb9 (2026-10-07, read-only git). Holdout snapshots data/holdouts/ (26 lists, newest 2026-10-07_778.txt + 2026-10-07_eqv_1590.txt). Sheet: data/sheet/2026-10-09_*.csv.…
reports/kill-forensics.md · 45 KB · updated Oct 9 21:57 · raw · ⤓
Results-tab status of those removals: (blank) 324, NONHALT 227, EQUIVALENCE 56, HALT 30, NONHALT (?) 1
reports/forensics/tables2.md · 27 KB · updated Oct 9 21:57 · raw · ⤓
Sections: S1. Proof-file style by era of first commit (median per file; proof files at the pin, certificates excluded) · S2. Same, split by assistant-style header / external-file references · S3. Files with an assistant-style header or references to files not in the repo · S4. Signal hit counts
reports/forensics/style_summary.md · 9 KB · updated Oct 9 21:57 · raw · ⤓
Sections: T1. Removals per window and reason (all mxdys windows since 4408) · T2. Kills per month by family (proofs: commit month of the attributed proof; eqv: month the list dropped the machine; Dec 2025+ windows) · T3. Kills per window by family (Dec 2025+, list-removal date) · T4. Proof structure per family (Dec 2025+ kills by proof) · T5. Who (commit author of the attributed proof, Dec 2025+) · T6. Sheet classification of killed machines (Dec 2025+) vs remaining
reports/forensics/tables.md · 18 KB · updated Oct 9 21:56 · raw · ⤓
Toolchain: opam 2.5.0, switch bb6, OCaml 4.14.2, Coq 8.20.1 with coq-native (COQ_NATIVE_COMPILER_DEFAULT=yes). Activate with eval $(opam env --switch=bb6).
reports/phase0_compile.md · 2 KB · updated Oct 9 17:12 · raw · ⤓