Imbad0202
diff --git a/‎expeditions/alphatensor-matmul.md‎
Lines changed: 2 additions & 2 deletions b/‎expeditions/alphatensor-matmul.md‎
Lines changed: 2 additions & 2 deletions
diff --git a/‎expeditions/busy-beaver-5.md‎
Lines changed: 2 additions & 2 deletions b/‎expeditions/busy-beaver-5.md‎
Lines changed: 2 additions & 2 deletions
@@ -12,7 +12,7 @@ result is not automatically the best one.
 
 **Statement.** How few scalar multiplications are needed to multiply two matrices? The school algorithm multiplies two n×n matrices with n³ scalar products; Strassen (1969) broke this for 2×2 with 7 instead of 8, and the question of the minimum for each fixed format has stayed open ever since. Concretely: what is the smallest R such that the matrix-multiplication tensor T_{n} decomposes as a sum of R rank-one triples u⊗v⊗w (this R, the tensor rank, equals the number of scalar multiplications in a bilinear algorithm)? AlphaTensor (DeepMind) reframed this as a single-player game and searched the decomposition space with a reinforcement-learning agent.
 
-**Answer (the verified deliverables).** Two figures are confirmed directly in the Nature paper: AlphaTensor multiplies 4×4 matrices over Z₂ (the field with two elements) using **47** multiplications, beating Strassen's two-level recursion which needs 7²=**49**; and it finds a rank-**76** decomposition of the T₄,₅,₅ product, improving the previous best of **80**. A third figure circulates widely — that AlphaTensor's 5×5-over-Z₂ algorithm used **96** multiplications and that Kauers & Moosbauer (JKU Linz) then cut it to **95** with a classical computer-aided search seeded by AlphaTensor's own algorithm. The pack author confirmed the **95** result and the "previous record was 96" framing first-party in the Kauers–Moosbauer source (arXiv:2210.04045), but did NOT find the **96** figure in the Nature paper's own text (which discusses T₅ only in standard arithmetic). So the over-claiming lesson stands on confirmed ground — a published record was improved within days — without resting on a number the Nature paper does not print. Mechanically correct ≠ optimal.
+**Answer (the verified deliverables).** Two figures are confirmed directly in the Nature paper: AlphaTensor multiplies 4×4 matrices over Z₂ (the field with two elements) using **47** multiplications, beating Strassen's two-level recursion which needs 7²=**49**; and it finds a rank-**76** decomposition of the T₄,₅,₅ product, improving the previous best of **80**. A third figure circulates widely — that AlphaTensor's 5×5-over-Z₂ algorithm used **96** multiplications and that Kauers & Moosbauer (JKU Linz) then cut it to **95** with a classical computer-aided search seeded by AlphaTensor's own algorithm. Both sources were read first-party: the **95** result and the "previous record was 96" framing are stated verbatim in Kauers–Moosbauer (arXiv:2210.04045), and the AlphaTensor Nature paper's own PMC open-access full text carries **no** 5×5-over-Z₂ count at all (its concrete finite-field figure is the 47 for 4×4). So the **96** is correctly attributed to K&M's framing of the prior record, not to AlphaTensor's paper, which does not print it. The over-claiming lesson stands on confirmed ground — a published record was improved within days — with the 96 sourced to where it is actually stated. Mechanically correct ≠ optimal.
 
 **Accessibility note.** The *audit* is unusually accessible even though producing the algorithm is not: a bilinear matrix-multiplication algorithm is correct if and only if its R rank-one triples sum to the matrix-multiplication tensor. That is a finite, mechanical identity you can verify by direct computation, with no trust in the search process required. The hard part — finding a low-rank decomposition in an astronomically large discrete space — is what AI-class search delivered; the correctness check is grade-school arithmetic over a finite field. This split (cheap to verify, expensive to find) is exactly what makes it a clean auditing target.
 
@@ -41,7 +41,7 @@ Dead end 4 — *Reading one Kauers-Moosbauer paper as covering everything.* Thei
 **First-party check — what I read directly vs could not confirm.**
 - Read directly from Nature/PMC: "AlphaTensor finds an algorithm for multiplying 4×4 matrices using 47 multiplications in Z2 … Strassen's two-level algorithm, which involves 7²=49 multiplications"; "rank-76 decomposition of T_{4,5,5}, improving over the previous state-of-the-art complexity of 80"; the tensor-decomposition correctness statement. Confirmed: Nature vol. 610, pp. 47–53, October 2022.
 - Read directly from arXiv:2210.04045 abstract: the prior announced 5×5-over-Z₂ result was **96** multiplications; Kauers & Moosbauer achieve **95**; submitted 8 Oct 2022; authors Kauers and Moosbauer.
-- Could NOT confirm directly from the Nature text I fetched: the explicit "**96** for 5×5 over Z₂" figure as printed in the Nature paper itself — I have it via the Kauers-Moosbauer paper's framing of "the previous record," not from the Nature full text I read. Treat as confirmed-via-K&M, not confirmed-from-Nature-directly.
+- Settled first-party (2026-07-03, both sources read directly): the **96** for 5×5 over Z₂ is Kauers–Moosbauer's framing of "the previous record" (arXiv:2210.04045 abstract, verbatim: "an algorithm for multiplying 5×5-matrices over ℤ₂ with only 96 multiplications, two fewer than the previous record"), and it is **not printed in AlphaTensor's Nature paper** — the PMC open-access full text carries no 5×5-over-Z₂ multiplication count (its finite-field figure is 47 for 4×4). The 96 is confirmed-from-K&M and confirmed-absent-from-Nature, so the pack attributes it to K&M, not to AlphaTensor's paper.
 - Could NOT confirm first-party: the specific "5×5 standard arithmetic = 97" count and a specific "independent 4×4" count attributed to Kauers-Moosbauer in the candidate brief — the Flip Graphs abstract I read does not state these numbers; it only says formats (4,4,5) and (5,5,5) were improved in char 2 and arbitrary fields. Omitted from the answer.
 
 ## step_graph
 
@@ -35,7 +35,7 @@ The difficulty was never the champion — it was certifying that nothing beats i
 
 **How verified.** This is a formally *verified* result, not merely peer-reviewed: the entire pipeline — the TNF enumeration producing all 181,385,789 machines, the five deciders, the 13 individual non-halting proofs, and the prior values S(2), S(3), S(4), S(2,3) — was machine-checked in the Coq proof assistant ("proof by reflection" / native_compute). Per the paper, Coq-BB5 is 27,274 lines of Coq plus 638 lemmas (plus 10,553 imported lines from busycoq) and compiles in ~45 minutes on 13 cores. I corroborated the headline facts across the arXiv HTML, Scott Aaronson's blog, and the bbchallenge announcement; the value and machine counts are mutually consistent.
 
-**First-party check.** Read directly from the arXiv HTML and the bbchallenge forum: S(5) = 47,176,870; 181,385,789 TNF machines; five named deciders; 13 sporadic machines; champion found by Marxen & Buntrock in 1989; champion transition table; 27,274 lines of Coq; "first … in over 40 years and first ever formally verified"; S(4) = 107 by Brady 1983; prediction that S(6) "will never be proved"; proof completed 2 July 2024. I could NOT independently re-render the PDF body text (the PDF fetch returned binary object structure, not prose), so the line-count and lemma-count figures rest on the HTML extraction rather than a second textual read of the PDF.
+**First-party check.** Read directly from the arXiv HTML (arXiv:2509.12337) and the bbchallenge forum: S(5) = 47,176,870; 181,385,789 TNF machines; five named deciders; 13 sporadic machines; champion found by Marxen & Buntrock in 1989; champion transition table; 27,274 lines of Coq; "first … in over 40 years and first ever formally verified"; S(4) = 107 by Brady 1983; prediction that S(6) "will never be proved"; proof completed 2 July 2024. Re-confirmed against the arXiv HTML on 2026-07-03: S(5), the TNF count, and the exact phrase "13 Sporadic Machines" are in the paper body; the body names only three of them (Skelet #1, #10, #17) and does NOT print the full 13-machine list — that list is in the Coq-BB5 sources / bbchallenge records, so a runnable S5 check from pack material alone is not available for the ten unnamed holdouts. I could NOT independently re-render the PDF body text (the PDF fetch returned binary object structure, not prose), so the line-count and lemma-count figures rest on the HTML extraction rather than a second textual read of the PDF.
 
 ## step_graph
 
@@ -44,7 +44,7 @@ The difficulty was never the champion — it was certifying that nothing beats i
 - **S2 — Probe small cases to feel the explosion** `small_case_probe` Hand-check S(1)=1, S(2)=6, S(3)=21 (1960s), then S(4)=107 (Brady 1983). Watch the jump to 47,176,870 at n=5. Check: simulate the n=2/n=3 champions by hand and confirm the published step counts; confirm the growth is super-exponential, motivating why n=5 needed machines not pencils.
 - **S3 — Cut the search space before deciding anything** `representation_shift` Tree Normal Form (TNF) collapses ~16.7 trillion syntactic machines to 181,385,789 by removing unreachable transitions and symmetric relabelings. Check: confirm the enumeration is itself run *inside Coq* (so the "we considered all machines" claim is machine-checked, not asserted).
 - **S4 — Decompose "all non-halters" into sound partial deciders** `lemma_decomposition` Split the non-halting burden across five independently-proved deciders (Loops, NGramCPS, RepWL, FAR, WFAR), each a checkable lemma "if decider D accepts machine M, then M never halts." Check: each decider's soundness is a separate Coq theorem; a reader can audit one decider without the others.
-- **S5 — Write the abandonment condition for the automated sweep** `kill_criteria` The kill criterion is explicit: any machine no decider settles becomes a named holdout requiring an individual proof. This bounds the bespoke work to a finite enumerated residue (13 sporadic machines: Skelet #1, #10, #17, …) rather than an open-ended hunt. Check: the count of undecided machines is reported and finite; the paper supplies one machine-checked non-halting proof per holdout — this pack names three (Skelet #1, #10, #17); the full 13-machine list lives in the paper and bbchallenge records, not in this pack.
+- **S5 — Write the abandonment condition for the automated sweep** `kill_criteria` The kill criterion is explicit: any machine no decider settles becomes a named holdout requiring an individual proof. This bounds the bespoke work to a finite enumerated residue (13 sporadic machines: Skelet #1, #10, #17, …) rather than an open-ended hunt. Check: the count of undecided machines is reported and finite; the paper supplies one machine-checked non-halting proof per holdout. First-party (arXiv:2509.12337, 2026-07-03): the paper's body states "13 Sporadic Machines" verbatim but names only three (Skelet #1, #10, #17); the full 13-machine list is not enumerated in the paper prose — it lives in the Coq-BB5 sources and the bbchallenge records, not in the paper body and not in this pack.
 - **S6 — Recast the summit as a verifiable chain** `milestone_rewrite` The claim "S(5)=47,176,870" becomes: (a) the champion halts at exactly 47,176,870 steps; (b) TNF covers all machines; (c) every machine is either decided non-halting by some sound decider, halts at ≤ 47,176,870, or is one of the 13 hand-proved non-halters. All assembled and checked in Coq. Check: each conjunct is a distinct Coq statement; the top theorem is their composition, auditable clause by clause.
 - **S7 — Confirm the boundary: why S(6) is different** `kill_criteria` Apply the same kill criterion at n=6 and watch it fail: ~2,600 holdouts remain, some (Antihydra) equivalent to open Collatz-type conjectures; the paper predicts S(6) "will never be proved." Check: confirm at least one S(6) holdout is reduced to a recognized open problem, establishing that S(5) sat exactly at the edge of decidability-by-effort.