TMBR: January 2026: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) →Holdouts: Added citation for confirmation in Rocq |
RobinCodes (talk | contribs) |
||
| Line 33: | Line 33: | ||
** @Peacemaker II [https://discord.com/channels/960643023006490684/1239205785913790465/1466337165305974806 found] two machines to halt with a bespoke [[accelerated simulator]]. | ** @Peacemaker II [https://discord.com/channels/960643023006490684/1239205785913790465/1466337165305974806 found] two machines to halt with a bespoke [[accelerated simulator]]. | ||
** @mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1466438332677619956 released] a [[holdouts list]] of 1314 machines up to equivalence, which is a 1% reduction (12 machines) from last month | ** @mxdys [https://discord.com/channels/960643023006490684/1239205785913790465/1466438332677619956 released] a [[holdouts list]] of 1314 machines up to equivalence, which is a 1% reduction (12 machines) from last month | ||
** @mxdys [https://discord.com/channels/960643023006490684/1460495597386731643/1466440885700006123 announced] the start of translating three proofs for halting machines into [[wikipedia:Rocq|Rocq]] (two machines found by @Peacemaker II this month, one proof for [[1RB0RC 0LC0LB 0LD1LC 0LE1LA 0LF--- 1RF1RA|a machine]] found to halt by | ** @mxdys [https://discord.com/channels/960643023006490684/1460495597386731643/1466440885700006123 announced] the start of translating three proofs for halting machines into [[wikipedia:Rocq|Rocq]] (two machines found by @Peacemaker II this month, one proof for [[1RB0RC 0LC0LB 0LD1LC 0LE1LA 0LF--- 1RF1RA|a machine]] found to halt by Racheline in July 2024) | ||
*[[BB(7)]]: | *[[BB(7)]]: | ||
**Andrew Ducharme further continued reducing the number of holdouts, from 20,387,509 to '''20,197,978''' TMs, a 0.93% reduction. This puts the total compute time on the current BB(7) pipeline just over '''50,000''' hours.<sup>[https://discord.com/channels/960643023006490684/1369339127652159509/1459719965396566078]</sup> | **Andrew Ducharme further continued reducing the number of holdouts, from 20,387,509 to '''20,197,978''' TMs, a 0.93% reduction. This puts the total compute time on the current BB(7) pipeline just over '''50,000''' hours.<sup>[https://discord.com/channels/960643023006490684/1369339127652159509/1459719965396566078]</sup> | ||
Revision as of 18:11, 2 February 2026
| Prev: December 2025 | This Month in Beaver Research | Next: February 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 is the first edition of TMBR in 2026.
TODO: mxdys released C++ implementation of FAR decider on 1/18
Champions
- nickdrozd discovered a new BLB(3,3) champion (
1RB2RB1LA_2LC0LB2LB_2RC2RA0LC(bbch)) which blanks the tape after running for more than 1042,745 steps. - creeperman7002 discovered
1TB1PA_1PC0PA_1TA0PD_---1TA, a TT(4,2) TM which runs for 48,186 steps and1TA2PB3TB---_3TA1PB1TA1PA, a TT(2,4) TM which runs for more than 3.467*1015 steps. - A new lower bound of was computed for the BBλ(91) champion.
Blog Posts
- 16 Jan 2026. Nick Drozd. AI Reproduction of Lin's Busy Beaver Proof.
- 28 Jan 2026. John Tromp. The largest number representable in 64 bits - Revised.
BB Adjacent
- Uniform-Action Busy Beavers were introduced, and lower bounds have been given up to BBu(6) (with BBu(2)=6, BBu(3)=17 and BBu(4)=29)
Theory
@ConePine shared an idea on how the value of BB(5) can be proved without enumerating Turing machines.
Holdouts
- BB(6): 2 [Needs update] solved machines.
- Progress has been made in reducing the list of machines not simulated up to 1e13, by Alistaire: see spreadsheet. Current count: 210. (Total reduction: 68. 38 machines[1][2][3][4][5][6][7][8][9][10][11][12][13][11 more][4 more][10 more][11 more][17 more] simulated out, plus 2 solved machines).
- Alistaire found a halting machine in the list mentioned above, see Discord. Approximate score: 4e12. Later, he found another halting machine in the same list, see Discord - approximate score: 1.5e18.
- @mxdys shared a list of machines that seem to be provable. See Discord.
- @Peacemaker II found two machines to halt with a bespoke accelerated simulator.
- @mxdys released a holdouts list of 1314 machines up to equivalence, which is a 1% reduction (12 machines) from last month
- @mxdys announced the start of translating three proofs for halting machines into Rocq (two machines found by @Peacemaker II this month, one proof for a machine found to halt by Racheline in July 2024)
- BB(7):
- Andrew Ducharme further continued reducing the number of holdouts, from 20,387,509 to 20,197,978 TMs, a 0.93% reduction. This puts the total compute time on the current BB(7) pipeline just over 50,000 hours.[1]
- The holdout count was further reduced to 19,879,953 (a 1.57% reduction), which breaks the 20 million barrier.[2]
- Another reduction brought the holdout count down to 19,781,295, a 0.5% reduction, then 19,303,801, a 2.41% reduction.
- BB(2,5):
- Andrew Ducharme found a machine to be nonhalting via @mxdys's FAR decider, which was confirmed in Rocq.
- BB(2,6):
- Andrew Ducharme reduced the number of holdouts from 870,085 to 867,008, a 0.35% reduction, with more application of Enumerate.py.
- Using the newly released mxdys FAR decider, the holdout count was brought down to 558,039, a 35.6% reduction.[3]