3x7 Collatz machine, longitudinal analysis

1RB2LB---_1RC2RB1LC_0LA0RB1LB (u.h.id. 642) does not halt

1RB2LB0LC_2LA2RA1RB_---2LA1LC (u.h.id. 650) does not halt

1RB1LC1LC_1LA2RB0RB_2LB---0LA (u.h.id. 412) does not halt

Coq verification of "BB(2,4) = 3,932,964"

BB(1094) > Loader's number

1RB1LA_1RC0RC_1LA1RD_1LE1RD_---1LF_1LE0LA halts in about 10^36 steps

Formal verification of TNF enumeration

Potential cryptid with new mechanism

Formal verification of "BB(2,4) = 3,932,964"

Skelet #17 is irregular

Lean formalisation of Busy beavers

1RB2LA0LA_2LC---2RA_0RA2RC1LC doesn't halt

Antihydra: first BB(6) Cryptid

2-symbol TM compiler

Reproduction of RepWL_ES

Coq-BB5 - Skelet #17 doesn't halt, Coq proof

Coq-BB5 - Complete Coq proof of "BB(5) = 47,176,870"

Write-up of Bouncers

Reproduction of savask's and mei's bouncers

Coq-BB5

Coq-BB5 - Repeated block decider (RepWL_ES)

Coq-BB5 - Reproduction and improvements on NGramCPS

Skelet #17 does not halt

Skelet #26 and #15 don't halt

Skelet #33 doesn't halt

Reproduction of Halting Segment

Reproduction of Backward Reasoning

Meet-in-the-Middle Weighted FAR (MITMWFAR)

Reproduction, optimization, formal verification of savask's bouncers

Coq verification of Backward Reasoning

Skelet #1 is a translated cycler – Coq agrees

Coq verification of Translated Cyclers

Coq verification of Cyclers

busycoq

Reproduction and variations on Bouncers (Iijil)

Reproduction and variations on Bouncers (savask)

BB(2,4) = 3,932,964

Reproduction of FAR

Write-up of Finite Automata Reduction

Machine #10756090, also known as Finned 3, is irregular

Skelet #1 is infinite ... we think

n-GRAM Closed Position Set

Reproduction of FAR

Write-up of Halting Segment

Implementation of Closed Position Set (CPS)

Bouncers

Reproduction of Halting Segment

Reproduction of Halting Segment

SAT-based FAR implementation

Reverse engineering of Skelet's CPS

Finite Automata Reduction (FAR)

Reproduction and debugging of Backward Reasoning

Bruteforce Closed Tape Language (CTL)

Reproduction of Cyclers

Reproduction of Translated Cyclers

Closed Tape Language (CTL) verifier

Dafny verification of Halting Segment

Dafny verification of Cyclers

Reproduction of Halting Segment and forward implem

Halting Segment (HS)

Closed Tape Language (CTL) SAT Solver

Write-up of Backward Reasoning

Write-up of Translated Cyclers

Write-up of Cyclers

Correctness of bbchallenge's deciders

Cyclers

Backward Reasoning (BR)

Translated Cyclers (TCs)

bbchallenge.org initial release

bbchallenge seed db

BB(2,4) champion found: 1RB2LA1RA1RA_1LB1LA3RB1RZ

bbfind - Skelet's 43 holdouts

bbfind - Closed Position Set (CPS)

(external) bbfind