TMBR: January 2026: Difference between revisions
Jump to navigation
Jump to search
RobinCodes (talk | contribs) →Holdouts: Finalized BB(6) holdouts section |
RobinCodes (talk | contribs) →Holdouts: Added clarification for informal holdout count discrepancy |
||
| (4 intermediate revisions by 2 users not shown) | |||
| Line 5: | Line 5: | ||
This is the first edition of TMBR in 2026. | This is the first edition of TMBR in 2026. | ||
TODO: mxdys released C++ implementation of FAR decider [https://discord.com/channels/960643023006490684/1239205785913790465/1462674863398326362 on 1/18] | TODO: mxdys released C++ implementation of FAR decider [https://discord.com/channels/960643023006490684/1239205785913790465/1462674863398326362 on 1/18], also add [[Code repositories]] page (is the FAR decider present there?) | ||
== Champions == | == Champions == | ||
| Line 12: | Line 12: | ||
* creeperman7002 discovered <code>1TB1PA_1PC0PA_1TA0PD_---1TA</code>, a [[TT|TT(4,2)]] TM which runs for 48,186 steps and <code>1TA2PB3TB---_3TA1PB1TA1PA</code>, a [[TT|TT(2,4)]] TM which runs for more than 3.467*10<sup>15</sup> steps. | * creeperman7002 discovered <code>1TB1PA_1PC0PA_1TA0PD_---1TA</code>, a [[TT|TT(4,2)]] TM which runs for 48,186 steps and <code>1TA2PB3TB---_3TA1PB1TA1PA</code>, a [[TT|TT(2,4)]] TM which runs for more than 3.467*10<sup>15</sup> steps. | ||
* A new lower bound of <math>f_{\varepsilon_0 \omega^{\omega^{3}}}\left(4\right)</math> was computed for the [[Busy Beaver for lambda calculus#Champions|BBλ(91)]] champion. | * A new lower bound of <math>f_{\varepsilon_0 \omega^{\omega^{3}}}\left(4\right)</math> was computed for the [[Busy Beaver for lambda calculus#Champions|BBλ(91)]] champion. | ||
* New champions were discovered for BBλ(61), BBλ(86), BBλ(90), BBλ(94), BBλ(96) and BBλ(100). | |||
== Blog Posts == | == Blog Posts == | ||
| Line 27: | Line 28: | ||
== Holdouts == | == Holdouts == | ||
{| class="wikitable" | |||
|+BB Holdout Reduction by Domain | |||
!Domain | |||
!New Holdout Count | |||
!Previous Holdout Count | |||
!Holdout Reduction | |||
!% Reduction | |||
|- | |||
|[[BB(2,5)]] | |||
|74 | |||
|75 | |||
|1 | |||
|1.3% | |||
|- | |||
|[[BB(6)]] | |||
|1314 | |||
|1326 | |||
|12 | |||
|0.9% | |||
|- | |||
|[[BB(7)]] | |||
|19,303,801 | |||
|20,387,509 | |||
|1,083,708 | |||
|5.32% | |||
|- | |||
|[[BB(2,6)]] | |||
|558,039 | |||
|870,085 | |||
|312,046 | |||
|35.86% | |||
|} | |||
* [[BB(6)]]: '''15''' solved machines. 1311 holdouts. 2 informally solved this month. | * [[BB(6)]]: '''15''' solved machines. 1311 holdouts. 2 informally solved this month. | ||
** Progress has been made in reducing the list of machines not simulated up to 1e13, by Alistaire and aparker: see [https://docs.google.com/spreadsheets/d/1mMp8bAcTFT91j7azn72liX8NSTwc2E_ozKnOGTfRCfw/edit?gid=806905077#gid=806905077 spreadsheet]. Current count: '''205'''. (Total reduction: '''73''' (+1 later). 39 machines<sup>[https://discord.com/channels/960643023006490684/1456755170527543420/1456755170527543420 <nowiki>[1]</nowiki>][https://discord.com/channels/960643023006490684/1456757189787127971/1456757189787127971 <nowiki>[2]</nowiki>][https://discord.com/channels/960643023006490684/1456757980203585678/1456757980203585678 <nowiki>[3]</nowiki>][https://discord.com/channels/960643023006490684/1456758622762696815/1456758622762696815 <nowiki>[4]</nowiki>][https://discord.com/channels/960643023006490684/1456759118818971709/1456759118818971709 <nowiki>[5]</nowiki>][https://discord.com/channels/960643023006490684/1456761765688901724/1456761765688901724 <nowiki>[6]</nowiki>][https://discord.com/channels/960643023006490684/1456762231491657830/1456762231491657830 <nowiki>[7]</nowiki>][https://discord.com/channels/960643023006490684/1456310285462802587/1456760768472289321 <nowiki>[8]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1456932659740545217 <nowiki>[9]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1456933097009320089 <nowiki>[10]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1456933714629099593 <nowiki>[11]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1456934113943621653 <nowiki>[12]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457147385309565021 <nowiki>[13]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457409447084429594 <nowiki>[11 more]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457497643478683770 <nowiki>[4 more]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457644806984437760 <nowiki>[10 more]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457992404597739672 <nowiki>[11 more]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1458413343088840734 <nowiki>[17 more]</nowiki>][https://discord.com/channels/960643023006490684/1458063260959113279/1468676578455064742 <nowiki>[aparker's machine]</nowiki>]</sup> simulated out, plus 6 solved machines). | ** Progress has been made in reducing the list of machines not simulated up to 1e13, by Alistaire and aparker: see [https://docs.google.com/spreadsheets/d/1mMp8bAcTFT91j7azn72liX8NSTwc2E_ozKnOGTfRCfw/edit?gid=806905077#gid=806905077 spreadsheet]. Current count: '''205'''. (Total reduction: '''73''' (+1 later). 39 machines<sup>[https://discord.com/channels/960643023006490684/1456755170527543420/1456755170527543420 <nowiki>[1]</nowiki>][https://discord.com/channels/960643023006490684/1456757189787127971/1456757189787127971 <nowiki>[2]</nowiki>][https://discord.com/channels/960643023006490684/1456757980203585678/1456757980203585678 <nowiki>[3]</nowiki>][https://discord.com/channels/960643023006490684/1456758622762696815/1456758622762696815 <nowiki>[4]</nowiki>][https://discord.com/channels/960643023006490684/1456759118818971709/1456759118818971709 <nowiki>[5]</nowiki>][https://discord.com/channels/960643023006490684/1456761765688901724/1456761765688901724 <nowiki>[6]</nowiki>][https://discord.com/channels/960643023006490684/1456762231491657830/1456762231491657830 <nowiki>[7]</nowiki>][https://discord.com/channels/960643023006490684/1456310285462802587/1456760768472289321 <nowiki>[8]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1456932659740545217 <nowiki>[9]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1456933097009320089 <nowiki>[10]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1456933714629099593 <nowiki>[11]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1456934113943621653 <nowiki>[12]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457147385309565021 <nowiki>[13]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457409447084429594 <nowiki>[11 more]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457497643478683770 <nowiki>[4 more]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457644806984437760 <nowiki>[10 more]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1457992404597739672 <nowiki>[11 more]</nowiki>][https://discord.com/channels/960643023006490684/1239205785913790465/1458413343088840734 <nowiki>[17 more]</nowiki>][https://discord.com/channels/960643023006490684/1458063260959113279/1468676578455064742 <nowiki>[aparker's machine]</nowiki>]</sup> simulated out, plus 6 solved machines). | ||
| Line 34: | Line 67: | ||
** @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. 4 of these were not previously simulated up to 1e13 steps, thus that count has been lowered to 206. | ** @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. 4 of these were not previously simulated up to 1e13 steps, thus that count has been lowered to 206. | ||
** @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). | ** @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, which has previously been missed when accounting for the informal holdout count, therefore the informal holdout count is now one less). | ||
** All machines of the "Unknown" class have been simulated up to 1e13 steps, with aparker simulating the last machine to 1.15e13: [https://discord.com/channels/960643023006490684/1458063260959113279/1468676578455064742 Discord]. | ** All machines of the "Unknown" class have been simulated up to 1e13 steps, with aparker simulating the last machine to 1.15e13: [https://discord.com/channels/960643023006490684/1458063260959113279/1468676578455064742 Discord]. | ||
*[[BB(7)]]: | *[[BB(7)]]: | ||
| Line 41: | Line 74: | ||
**Another reduction brought the holdout count down to '''19,781,295''', a 0.5% reduction, then '''19,303,801''', a 2.41% reduction. | **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)]]: | *[[BB(2,5)]]: | ||
**Andrew Ducharme [https://discord.com/channels/960643023006490684/1259770421046411285/1466208979511414885 found] a machine to be nonhalting via @mxdys's FAR decider, which was [https://discord.com/channels/960643023006490684/1259770421046411285/1466331107279769736 confirmed in Rocq]. | **Andrew Ducharme '''[https://discord.com/channels/960643023006490684/1259770421046411285/1466208979511414885 found] a machine to be nonhalting via @mxdys's FAR decider''', which was [https://discord.com/channels/960643023006490684/1259770421046411285/1466331107279769736 confirmed in Rocq]. | ||
*[[BB(2,6)]]: | *[[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. | **Andrew Ducharme reduced the number of holdouts from 870,085 to '''867,008''', a 0.35% reduction, with more application of Enumerate.py. | ||
Latest revision as of 18:46, 15 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, also add Code repositories page (is the FAR decider present there?)
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.
- New champions were discovered for BBλ(61), BBλ(86), BBλ(90), BBλ(94), BBλ(96) and BBλ(100).
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
| Domain | New Holdout Count | Previous Holdout Count | Holdout Reduction | % Reduction |
|---|---|---|---|---|
| BB(2,5) | 74 | 75 | 1 | 1.3% |
| BB(6) | 1314 | 1326 | 12 | 0.9% |
| BB(7) | 19,303,801 | 20,387,509 | 1,083,708 | 5.32% |
| BB(2,6) | 558,039 | 870,085 | 312,046 | 35.86% |
- BB(6): 15 solved machines. 1311 holdouts. 2 informally solved this month.
- Progress has been made in reducing the list of machines not simulated up to 1e13, by Alistaire and aparker: see spreadsheet. Current count: 205. (Total reduction: 73 (+1 later). 39 machines[1][2][3][4][5][6][7][8][9][10][11][12][13][11 more][4 more][10 more][11 more][17 more][aparker's machine] simulated out, plus 6 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.
- Dyuan shared an informal proof for two machines nonhalting, using Longitudinal Analysis.
- @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. 4 of these were not previously simulated up to 1e13 steps, thus that count has been lowered to 206.
- @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, which has previously been missed when accounting for the informal holdout count, therefore the informal holdout count is now one less).
- All machines of the "Unknown" class have been simulated up to 1e13 steps, with aparker simulating the last machine to 1.15e13: Discord.
- 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]