TMBR: January 2026: Difference between revisions
Jump to navigation
Jump to search
Qwertyasdf (talk | contribs) →Holdouts: add solved 2,5 machine |
RobinCodes (talk | contribs) →Holdouts: Added all BB(6) progress |
||
| (8 intermediate revisions by 4 users not shown) | |||
| Line 4: | Line 4: | ||
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] | |||
== Champions == | == Champions == | ||
| Line 14: | Line 16: | ||
* 16 Jan 2026. Nick Drozd. [https://nickdrozd.github.io/2026/01/16/ai-lin-busy-beaver.html AI Reproduction of Lin's Busy Beaver Proof]. | * 16 Jan 2026. Nick Drozd. [https://nickdrozd.github.io/2026/01/16/ai-lin-busy-beaver.html AI Reproduction of Lin's Busy Beaver Proof]. | ||
* 28 Jan 2026. John Tromp. [https://tromp.github.io/blog/2026/01/28/largest-number-revised The largest number representable in 64 bits - Revised]. | |||
== BB Adjacent == | == BB Adjacent == | ||
| Line 24: | Line 27: | ||
== Holdouts == | == Holdouts == | ||
* [[BB(6)]]: ''' | * [[BB(6)]]: '''15''' solved machines. 1311 holdouts (3 informally solved this month, one informally solved earlier). | ||
** Progress has been made in reducing the list of machines not simulated up to 1e13, by Alistaire: see [https://docs.google.com/spreadsheets/d/1mMp8bAcTFT91j7azn72liX8NSTwc2E_ozKnOGTfRCfw/edit?gid=806905077#gid=806905077 spreadsheet]. Current count: '''210'''. (Total reduction: '''68'''. 38 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>]</sup> simulated out, plus 2 solved machines). | ** Progress has been made in reducing the list of machines not simulated up to 1e13, by Alistaire: see [https://docs.google.com/spreadsheets/d/1mMp8bAcTFT91j7azn72liX8NSTwc2E_ozKnOGTfRCfw/edit?gid=806905077#gid=806905077 spreadsheet]. Current count: '''210'''. (Total reduction: '''68''' (+1 later). 38 (+1) 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>]</sup> simulated out, plus 2 solved machines). | ||
** Alistaire found a halting machine in the list mentioned above, see [https://discord.com/channels/960643023006490684/1239205785913790465/1456317703156531211 Discord]. Approximate score: 4e12. Later, he found another halting machine in the same list, see [https://discord.com/channels/960643023006490684/1239205785913790465/1456381492019069192 Discord] - approximate score: 1.5e18. | ** Alistaire found a halting machine in the list mentioned above, see [https://discord.com/channels/960643023006490684/1239205785913790465/1456317703156531211 Discord]. Approximate score: 4e12. Later, he found another halting machine in the same list, see [https://discord.com/channels/960643023006490684/1239205785913790465/1456381492019069192 Discord] - approximate score: 1.5e18. | ||
** @mxdys shared a list of machines that seem to be provable. See [https://discord.com/channels/960643023006490684/1460495597386731643/1460495597386731643 Discord]. | ** @mxdys shared a list of machines that seem to be provable. See [https://discord.com/channels/960643023006490684/1460495597386731643/1460495597386731643 Discord]. | ||
** @Peacemaker II [https://discord.com/channels/960643023006490684/1239205785913790465/1466337165305974806 found] | ** Dyuan [https://discord.com/channels/960643023006490684/1460495597386731643/1463044134263853066 shared an informal proof] for a machine nonhalting, using [[Longitudinal Analysis]]. | ||
** @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 | ** @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/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). | |||
** 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)]]: | ||
**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> | ||
| Line 35: | Line 41: | ||
**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. | **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 ''' | **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.[https://discord.com/channels/960643023006490684/1084047886494470185/1467385975704391897] | ||
[[Category:This Month in Beaver Research|2025-12]] | [[Category:This Month in Beaver Research|2025-12]] | ||
Latest revision as of 19:09, 4 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): 15 solved machines. 1311 holdouts (3 informally solved this month, one informally solved earlier).
- 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 (+1 later). 38 (+1) 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.
- Dyuan shared an informal proof for a machine 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).
- 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]