TMBR: November 2026: Difference between revisions
Jump to navigation
Jump to search
BB(2,5) holdouts list Rocq-confirmed |
precisions about holdout status change in BB(2,5) |
||
| Line 77: | Line 77: | ||
|37 (official) | |37 (official) | ||
|59 (official), 37 (informal) | |59 (official), 37 (informal) | ||
|22 ( | |22 (Rocq confirmation of Lean proofs) | ||
|37.29% | |37.29% (confirmations) | ||
|} | |} | ||
| Line 84: | Line 84: | ||
** On November 1, Ahmer Raza simulated two holdouts, both Reus Vampires, to halting.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1566293610503340184]</sup> | ** On November 1, Ahmer Raza simulated two holdouts, both Reus Vampires, to halting.<sup>[https://discord.com/channels/960643023006490684/1239205785913790465/1566293610503340184]</sup> | ||
*[[BB(2,5)]] | *[[BB(2,5)]] | ||
** On November 3, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of 37 holdouts.<sup>[https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584]</sup> | ** On November 3, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of '''37''' holdouts.<sup>[https://discord.com/channels/960643023006490684/1259770421046411285/1567052029430595584]</sup> | ||
== Cryptids == | == Cryptids == | ||
Revision as of 13:22, 3 November 2026
| Prev: October 2026 | This Month in Beaver Research | Next: December 2026 |
This edition of TMBR is in progress and has not yet been released. Please add any notes you think may be relevant (including in the form a of a TODO with a link to any relevant Discord discussion).
This Month in Beaver Research for November 2026.
BB Adjacent
- Pebble Automaton
- On November 2, the remaining group of 22 pebble(11) holdouts was officially dubbed the "golems". They are modeled by complex systems of equations, making them potential cryptids. They can be categorized into 7 unique paths.
Champions
| Domain | Champion | Discoverer | New lower bound | Discoverer | Previous lower bound |
|---|---|---|---|---|---|
| BB(20) | 1RR---_0LJ0RC_1RB1LD_0LD1LE_1LF1RG_1LI0LE_0RE1LD_1RB1RH_1RH1RN_1LK1LJ_0LL1LJ_1RM1RA_0RM0RH_0LO1RN_1LP0LP_1RH1LQ_1LO1LO_1LS1RR_1RZ1LT_0LH0LS (bbch)
|
User:Jacobzheng | User:Jacobzheng | ||
| BB(11,4) | 1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK (bbch)
|
User:Loader3229 | |||
| BB(8,5) | 2RG3LB4LC2RA4LB_1RZ---1LD2RA4LD_3RB1LB3LC2RC4LC_3RE---3LC2RC3LC_---3RE4LE4LH4RB_4LE3LG3LB2RF4LG_2LH3RG1LH2RF2RA_3RG1LG3LH2RH4LH (bbch)
|
User:Loader3229 | |||
| BB(4,6) | 5LD3LB5LC2RA4LB4LC_1RZ3RB1LC2RA3RD0LA_3RB1LB3LC2RC4LC1RA_3RB0LA2LC4LD4LC4LD (bbch)
|
||||
| BB(5,6) | 1LE3LB2LA2RA4LB5RA_1RZ3RB1LC2RA3RD4RA_3RB1LB3LC2RC4LC2LB_3RB0LA5LE4LD4LC4LD_4LC5LC0RE5LE1RE2RE (bbch)
|
||||
| BB(6,6) | 5RB3LB1RZ2RA4LB---_2LC3RB1LD2RA3LF---_3RB1LB3LC2RC4LC0LE_3RB3RD3LC2RC---3RE_5RC3RE1RB4LC------_5RB------1LF------ (bbch)
|
||||
| BB(7,6) | 2LF3LB1RZ2RA4LB3LD_3LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE---4LC3LG5LE_5RB5RB0LF1LF---5LF_5LF------1LG---5LG (bbch)
|
- User:Loader3229 discovered an array of champions based on Kropitz's current BB(3,4) champion, demonstrating the following bounds:
- On November 2, User:Jacobzheng discovered a machine that demonstrates the lower bound BB(20) > .
Holdouts
| Domain | New Holdout Count | Previous Holdout Count | Holdout Reduction | % Reduction |
|---|---|---|---|---|
| BB(6) | 608 | 608 | 0 | 0.00% |
| BB(2,5) | 37 (official) | 59 (official), 37 (informal) | 22 (Rocq confirmation of Lean proofs) | 37.29% (confirmations) |
- BB(6)
- On November 1, Ahmer Raza simulated two holdouts, both Reus Vampires, to halting.[3]
- BB(2,5)
- On November 3, mxdys confirmed in Rocq the proofs in Lean of 22 TMs solved with AI assistance (GPT6 and Aristotle), releasing a formal list of 37 holdouts.[4]
Cryptids
All Turing machines mentioned in this section work with an alphabet of 2 symbols unless explicitly stated. The state bounds given also only consider Turing machines which work with 2 symbols.
- Cryptids in the Wild (+ Energy Vampires)
- Reus Vampires
- On November 1, Ahmer Raza ran path O4 to 1,941,376,761,248 iterations, at which point it halts![5] This path corresponds to a group of machines with halting times of over 10683,718,950,000 steps, and decides the last of the 7 Reus vampires.
- Reus Vampires
- Larger Cryptids
- Logical Independence
- Zermelo-Frankel set theory
- On November 1, charlie claimed to have used Claude to formally reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition).
- Zermelo-Frankel set theory
- Computational Complexity Theory
- On November 1, GregoryMorse claimed to have found a 278-state machine that quasihalts iff P = NP, a 295-state machine that quasihalts iff P = PP, and a 291-state machine that quasihalts iff P = PSPACE.[6]
- Logical Independence
| Conjecture | Domain | Discoverer | Discovery date | Notes |
|---|---|---|---|---|
| Pillai's conjecture | BBBB(91) | charlie, Claude[7] | November 1 | Unknown - pseudoquasihalts if the conjecture is false. Proof. |