TMBR: October 2026 - BusyBeaverWiki

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 October 2026.

Papers

• Research entity Google DeepMind published a paper on the usage of AI to derive simple arithmetic rules for small Turing machine holdouts.^[1]

Blog Posts

• Blanking Beavers: Results and Open Problems. Nick Drozd. 20 Oct 2026.

BB Adjacent

• Register Machine
  • On October 1, sheep discovered a 12-state, 2-register Cryptid which halts iff 7 converges to 1 under the Collatz-like 5n+1 map, thus showing that MBB(12, 2) is hard.^[2]
  • On the same day, @-d enumerated MBB(8), which left 7,891 holdouts after reduction, or 404 holdouts if an ai-created decider is used.^[3]
  • On the same day, @mineralli discovered a family of champions for MBB(n, 1).^[4]
  • On October 2, @mineralli discovered a new champion for MBB(10, 2).^[5]
  • On the same day, sheep discovered 2 new tetrational champions for MBB(10).^[6][7]
  • On the same day, Shawn Ligocki released an MBB(8) holdout list consisting of 145 holdouts,^[8] using another ai-created decider similar to CTL.^[9]
  • On October 3, Shawn Ligocki released another MBB(8) holdout list consisting of 46 holdouts,^[10] later reduced to 6^[11] (from 7^[12]) holdouts.
  • On the same day, Shawn Ligocki discovered a cryptid similar to Space Needle amongst the 6 remaining holdouts, showing MBB(8) is hard.^[13]
  • On the same day, sheep analyzed the rest of the holdouts, discovering 4 equivalences and another Space Needle-like cryptid (Needle 1),^[14] meaning MBB(8) "probviously" = 3,394.
  • On the same day, Katelyn Doucette devised a method to show that a sizeable portion of powers of two could not be reached by Needle 1's path.^[15] She later concluded that this backwards reasoning-like method, though powerful, would not be enough to decide Needle 1.^[16]
  • On October 7, sheep rediscovered a 2003 dissertation by Rick Griffiths^[17] which investigated the (maximum register value) Busy Beaver function for register machines (Beaver(n)); Griffiths determines the values of Beaver(n) for sizes 1 to 4 (using the modern instruction counting convention), and provides lower bounds for sizes 5 to 8. It also provides a machine (constructed by Ortwin Gasper in 2003) which shows the bound MBB(11) > 10↑↑17.74.^[18]
  • On October 8, sheep marginally improved the bounds for MBB(10).^[19]
  • On October 10, AlephSquirrel rediscovered a 2020 article by Yuri Matiyasevich^[20] which provides a 130-instruction, 29-register machine which halts if and only if the Riemann hypothesis is false.^[21]
  • On October 17, mineralli published a script capable of converting any arbitrary register machine into an equivalent 2-register machine.^[22]
  • On October 22, mineralli released a list of 581 MBB(11, 2) holdouts (though they are not confident that these are all of the MBB(11, 2) holdouts) that display Collatz-like behavior.^[23]
• SKI Calculus
  • On October 8, cppdecksucker shared a holdouts list for Ξ₀_SK(8) consisting of 17 terms, 2 of which have been decided to not have a normal form.^[24]
  • On October 12, cppdecksucker claimed to have used Aristotle AI to prove Ξ₀_SK(8) = 80.^[25]
  • On the same day, Δ⁵ proved Ξ₀_BCKW(5) = 47.^[26]
  • On October 13, Δ⁵ translated a 15 combinator term in the BCKW calculus, demonstrating Ξ₀_BCKW(15) > ${\displaystyle f_{{\omega }^{2\uparrow \uparrow 18-1}}(2)}$.^[27]
  • On October 20, elgan65536 discovered new champions for Ξ₀(9)^[28] and Ξ₀_SK(11),^[29], with trivial extensions that are new champions for Ξ₀(10), Ξ₀(11), and Ξ₀_SK(12).^[30]
  • On October 21, elgan65536 discovered a new champion for Ξ₀_SK(10).^[31]
• Lambda Calculus
  • On October 9, Discord user Sam discovered a new 80 bit term,^[32] shown by 50_ft_lock to demonstrate the bound BBλ(80) > ${\displaystyle f_{{\omega }^{\omega }+1}(3)}$.^[33]
  • On October 13, Sam optimized the BBλ(80) champion to a reduced and improved 79 bit term, demonstrating the bound BBλ(79) > ${\displaystyle f_{{\omega }^{\omega }+1}(7)}$.^[34]
  • On the same day, Gustavo Melo estimated that a specific family of terms, mentioned earlier by Sam,^[35] reaches ${\displaystyle f_{{\omega }^{\omega }\cdot 2+1}}$ growth.^[36]
  • On the same day, Sam discovered new ${\displaystyle f_{{\omega }^{\omega }\cdot 2+1}}$-level champions for BBλ(70), BBλ(74), BBλ(78), and BBλ(80).^[37]
  • On October 15, Gustavo Melo discovered new ${\displaystyle f_{{\omega }^{{\omega }^{\omega }}}}$-level champions for BBλ(77),^[38] BBλ(80),^[39] and BBλ(85) (the next day),^[40] and conjectured that a specific 76 bit term would have a normal form greater than ${\displaystyle f_{{\omega }^{{\omega }^3}}(2)}$ bits.^[41]
  • On October 16, Δ⁵ discovered a new 80 bit term, demonstrating the bound BBλ(80) > ${\displaystyle f_{{\omega }^{{\omega }^{14}}}(2)}$.^[42][43]
  • On the same day, Gustavo Melo proved the conjecture about the 76 bit term's size, demonstrating the bound BBλ(76) > ${\displaystyle f_{{\omega }^{{\omega }^3}}(2)}$.^[44]
  • On October 17, Δ⁵ discovered a new 77 bit term, demonstrating the bound BBλ(77) > ${\displaystyle f_{{\omega }^{\omega \cdot 2}}(3)}$.^[45]
  • On October 18, Δ⁵ discovered a new 82 bit term, demonstrating the bound BBλ(82) > ${\displaystyle f_{{\omega }^{{\omega }^{\omega }}}(2\uparrow \uparrow \uparrow \uparrow 18)}$.^[46]
• Domain-Restricted Instruction-Limited Busy Beaver
  • On October 10, star claimed to have used Claude to discover a new champion for BBi(10, 6, 2) (colloquially known as BB(5.5)).^[47]
  • On October 11, star claimed to have used Claude to reduce BBi(10, 6, 2) to 4 holdouts,^[48] all of which were present in the most recent holdouts equivalence list at the time (BB6_holdouts_1581_eqv_740.txt).^[49] She believes that two of these holdouts (1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF (bbch) and another equivalent machine) are Cryptids.^[50]
• Fractran
  • On October 13, @-d completed the verification of the ai-generated 1dpc decider and its certificates, reducing the official count of BBf(23) holdouts from 21,233 to 8,021, and the official count of BBf(24) holdouts from 231,432 to 85,726.^[51]
  • On the same day, @-d discovered 0.1% of certificates created by the ai-generated ndpc decider to be invalid, hypothesized to have been caused by a soundness bug in the decider.^[52]
• Pebble Automaton
  • On October 13, AlephSquirrel proved peBBle(5) = 11 and peBBle(6) = 17.^[53]
  • On October 18, AlephSquirrel proved peBBle(7) = 28.^[54]
  • On October 19, Shawn Ligocki claimed to have used Google Gemini to prove peBBle(8) = 63 using a CTL-like method,^[55] and to find 54,394 9-pebble holdouts (including automata with multiple undefined transitions),^[56] later reduced to 376 holdouts,^[57] then 104 holdouts.^[58]
  • On October 19, a poll was held to determine whether a pebble automata that moves pebbles every step, but has no effect on any cells (i.e. it has a static tape), should be considered as halted (which is what the old halting definition decides); the general consensus is to class this behavior as non-halting.^[59]
  • On the same day, Shawn Ligocki claimed to have used Google Gemini to prove peBBle(9) = 63,577, under the old halting definition.^[60]
  • On October 20, Shawn Ligocki claimed to have used Google Gemini to find a peBBle(10) champion that runs for 5,778 steps, simultaneously finding 1,867 10-pebble holdouts (including automata with multiple undefined transitions),^[61] later reduced to 1,221 holdouts, though these lists were considered only under the old halting definition.^[62]
  • On the same day, AlephSquirrel discovered that one of the peBBle(10) holdouts used a mechanism that simulates a Piecewise Affine Function,^[63] though none of the extraneous conditions lead to halting;^[64] she also provided a compressed spacetime diagram of this holdout.^[65] A similar holdout was shared earlier that day by Shawn Ligocki, but not analyzed.^[66]
  • On the same day, Shawn Ligocki claimed to have used Google Gemini to produce peBBle(10) holdout lists with 429 holdouts,^[67] then 319 holdouts,^[68] both updated to account for the new halting definition.^[69]
  • On October 21, AlephSquirrel analyzed the aforementioned peBBle(10) former holdout (excluding edge cases), confirming that it models a PAF.^[70]
  • On the same day, Shawn Ligocki claimed to have used Google Gemini to produce peBBle(10) holdout lists with 268 holdouts.^[71]
  • On the same day, Aleph Squirrel discovered a 12 pebble possible Cryptid, implying solving peBBle(12) would be at least as hard as solving a BMO1-like problem.^[72]
  • On the same day, Shawn Ligocki claimed to have used Google Gemini to prove peBBle(10) = 5,778.^[73]
• Busy Bricklayer Problem
  • On October 20, mathmasterzach, along with their friends, showed that the problem's associated busy beaver function, over the 10-ominos, either takes the value 138, or is larger than 3,000.^[74] Note that there is still one undecided 10-omino.
  • On October 21, mathmasterzach, using the singular 10-omino holdout, produced a tiling of an 88-cell wide half-strip.^[75]

Champions

New champions discovered this month

m	n	BB(m, n)			BB(m, n) prior to October
		Champion	Discoverer	Lower bound	Discoverer	Lower bound
7	2	1RB0RG_1RC1RB_0RD1RZ_0LE0LD_0LF1LE_1RA1LF_1LC0RB (bbch)	Jeff Ketchersid	${\displaystyle 3{\uparrow }^{20}3}$	Pavel Kropitz	${\displaystyle 2{\uparrow }^{11}2{\uparrow }^{11}3}$
8	2	1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LH0LC_1RG1LD_0RG0RF_1RG--- (bbch)		${\displaystyle f_{\omega }^3(12)}$
9	2	1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LH0LC_1RG1LD_0RG0RF_0LI---_1LC0RA (bbch)		${\displaystyle f_{\omega }^6(12)}$	Jacobzheng	${\displaystyle f_{\omega }(f_9(2))}$
10	2	1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RZ0LC (bbch)		${\displaystyle f_{\omega +1}(2{\uparrow }^{36}3)>g_{64}}$	racheline	${\displaystyle f_{\omega }^2(25)}$
11	2				Jacobzheng	${\displaystyle f_{\omega }^2(10{\uparrow }^{4}4)}$
12	2	1RB0RA_1LC1LF_1RD0LB_1RA1LE_1LI0LC_0RG1LD_1RH1LG_1LC0RG_0LJ0LI_1RK0LC_0RL---_0RF1RZ (bbch)		${\displaystyle f_{\omega +1}^2(2{\uparrow }^{36}3)}$	racheline	${\displaystyle f_{\omega }^4(2\uparrow \uparrow \uparrow 4-3)>f_{\omega }^4(f_4(2))}$
13	2	1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_0LG1RI_1RE0RH_1LF0RC_1RM0LE_1LA1LE_0LL1LB_0RM1LL_1RZ1RH (bbch)		${\displaystyle f_{\omega +2}(f_{\omega }(20))}$	50_ft_lock	${\displaystyle f_{\omega +1}(2046)>g_{64}}$
14	2	1RB1RA_1RI1RC_0LD1LG_0RE1LD_1LN1RF_1LJ0RA_1RA0LH_1LG1LH_1RK0LM_1RZ0LE_0LE0RJ_1LH1LM_0LH0LL_0LG1LN (bbch)		${\displaystyle f_{\omega +2}^3(15)}$	Jacobzheng	${\displaystyle f_{\omega +1}(f_{\omega }^4(f_7(3)))}$
2	7	1RB3RB4LA1LB5LA6LB5RA_2LA6RA4RB1RZ3LB6LA4RB (bbch)	roromachine14	${\displaystyle 10\uparrow \uparrow \uparrow 4}$	Pavel Kropitz	${\displaystyle 10\uparrow \uparrow 10\uparrow \uparrow 10^{10^{115}}}$
2	8	1RB3RB4LA1LB5LA6LB5RA1RZ_2LA6RA4RB7RA3LB6LA4RB4RA (bbch)		${\displaystyle 10\uparrow \uparrow \uparrow 5}$
2	9	1RB3RB4LA1LB5LA6LB5RA8RA1RZ_2LA6RA4RB7RA3LB6LA4RB4RA4RA (bbch)		${\displaystyle 10\uparrow \uparrow \uparrow 6}$

• Jeff Ketchersid claimed to have used Claude Opus 5.5 and Gemini 4 Argon to discover and prove the scores of a set of Ackermann-level machines, four of which (BB(8), BB(9), BB(10), BB(12)) were derived from Pavel Kropitz's former BB(7) champion, and two of which (BB(13), BB(14)) were derived from Jacobzheng's former champion for BB(14). Ketchersid also claimed to have found a new, novel champion for BB(7). Ketchersid's claimed bounds are listed here:
  • On October 4, BB(8) > ${\displaystyle 2{\uparrow }^{37}3}$.^[76][77] Prior to this, the BB(7) champion, found by Pavel Kropitz, which held the BB(8) championship by default, ran for around ${\displaystyle 2{\uparrow }^{11}2{\uparrow }^{11}3}$ steps.
  • On October 7, BB(9) > ${\displaystyle f_{\omega }(2{\uparrow }^{13}3)}$.^[78][79] Prior to October, the BB(9) champion, found by Jacobzheng, ran for around${\displaystyle f_{\omega }(f_9(2))}$ steps.
  • On October 8, BB(10) > ${\displaystyle f_{\omega +1}(2{\uparrow }^{36}3)}$.^[80][81] Prior to October, the BB(10) champion, found by racheline, ran for around ${\displaystyle f_{\omega }^2(25)}$ steps; this machine also dethroned the previous BB(11) champion, which was found by Jaconzheng, and ran around ${\displaystyle f_{\omega }^2(10{\uparrow }^{4}4)}$ steps. for This is also the smallest 2-symbol machine (in states) known to run for longer than a Graham's number number number of steps; in other words, this machine shows that BB(10) > g₆₄, improving on 50_ft_lock's earlier result that BB(13) > g₆₄.
  • On October 11, BB(12) > ${\displaystyle f_{\omega +1}^2(2{\uparrow }^{36}3)}$.^[82] Prior to October, the BB(12) champion, found by racheline, ran for around ${\displaystyle f_{\omega }^4(2\uparrow \uparrow \uparrow 4-3)}$ steps.
  • On October 14, BB(13) > ${\displaystyle f_{\omega +2}(f_{\omega }(20))}$ and BB(14) > ${\displaystyle f_{\omega +2}^3(15)}$.^[83][84] Prior to October, the BB(13) champion, found by 50_ft_lock, ran for around ${\displaystyle f_{\omega +1}(2046)}$ steps, and was previously the 2-symbol machine with the least amount of states used that was known to run longer than g₆₄ steps, whereas the BB(14) champion, found by Jacobzheng, ran for around ${\displaystyle f_{\omega +1}(f_{\omega }^4(f_7(3)))}$ steps.
  • On October 17, BB(9) > ${\displaystyle f_{\omega }(f_{\omega }(465,009))}$.^[85]
  • On October 18, BB(9) > ${\displaystyle f_{\omega }^3(12)}$.^[86]
  • On October 19, BB(8) > ${\displaystyle f_{\omega }^3(12)}$.^[87]
  • On October 22, a new bound for BB(9) slightly larger than that for BB(8) at the time.^[88]
  • On October 22, BB(9) > ${\displaystyle f_{\omega }^6(12)}$, with their new BB(8) champion from October 19 also being announced along with this champion on this day.^[89][90][91]
  • On October 23, BB(7) > ${\displaystyle 3{\uparrow }^{20}3}$.^[92][93] Prior to this, the aforementioned BB(7) champion, found by Pavel Kropitz, ran for around ${\displaystyle 2{\uparrow }^{11}2{\uparrow }^{11}3}$ steps.

• roromachine14 claimed to have used Gemini 4 Argon to discover new champions for BB(2,7), BB(2,8), and BB(2,9), running for at least ${\displaystyle 10\uparrow \uparrow \uparrow 4}$ steps, ${\displaystyle 10\uparrow \uparrow \uparrow 5}$ steps, and ${\displaystyle 10\uparrow \uparrow \uparrow 6}$ steps respectively.^[94][95] The previous champion for these domains was, by default, Pavel Kropitz's BB(2,6) champion, which ran for at least ${\displaystyle 10\uparrow \uparrow 10\uparrow \uparrow 10^{10^{115}}}$ steps.

Holdouts

BB Holdout Reduction by Domain

Domain	New Holdout Count	Previous Holdout Count	Holdout Reduction	% Reduction
BB(6)	663	797	134	16.81%
BB(4,3)	4,719,315	4,720,332	1,017	0.02%
BB(2,5)	37	39	2	5.13%
BB(2,6)	389,503	412,086	22,583	4.47%
BB(2,7)	3,125,433,611	Enumeration incomplete	N/A	N/A

• BB(6)
  • On October 1, Discord user oscar claimed to have used GPT-6.1 Sol to prove a machine non-halting, formalized in Rocq the next day.^[96]
  • On October 1, dyuan shared a subset of BB(6) holdouts, consisting of 24 machines which are expected to be easily analyzable by longitudinal analysis.^[97]
  • On October 3, oscar claimed to have used GPT-6.1 Sol to prove a machine halting,^[98] formalized in Rocq the next day.^[99]
  • On October 6, Discord user Zuck claimed to have used Claude to prove a machine non-halting.^[100]
  • On October 7, mxdys released a holdout list of 778 machines up to equivalence.^[101]
  • On October 10, Discord user Dennis claimed to have used Claude Opus 5.5 to prove a machine non-halting.^[102]
  • On the same day, mxdys released a holdout list of 740 machines up to equivalence.^[103]
  • On October 11, Dennis claimed to have used Claude Opus 5.5 to prove another 4 machines non-halting.^[104]
  • On October 13, Dennis claimed to have used Claude Opus 5.5 to prove another 3 machines non-halting.^[105]
  • On the same day, Dennis claimed to have used Claude Opus 5.5 to prove a machine halting.^[106]
  • On October 15, mxdys released a holdout list of 698 machines up to equivalence.^[107]
  • On the same day, Google DeepMind claimed to have used Gemini 3.1 Pro to prove 7 machines halting, and another 20 machines (pull requests #1, #2, #3, #4) non-halting.^[108]
  • On the same day, Dennis claimed to have used Claude Opus 5.5 and GPT-6 Astra to prove another 8 machines (pull requests #1, #2, #3, #4, #5) non-halting.^[109]
  • On October 16, mxdys released a holdout list of 663 machines up to equivalence.^[110]
  • On the same day, Re-us claimed to have used Claude Opus 5.5 to discover 7 probviously halting machines (described as energy vampires) which rely on an exceedingly rare tape configuration to halt, similar to the mechanism used by 1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA (bbch).^[111][112] Over the following few days, Re-us, Andrew Ducharme, and Ersen would continue to simulate 3 of the unique orbits (equivalent to 5 machines), confirming four of the machines do not halt within 10 billion rule applications.^{[113][114][115][116]} Re-us has also estimated that, assuming perfect randomness of the machines' bit generation, a median of 780 billion rule applications would have to be applied for each machine to halt.^[117][118]
  • On October 18, Ersen claimed to have used Claude to help run an independent (and currently ongoing) run of Antihydra to 2³⁸ rule applications, seemingly verifying apgoucher's results.^[119][120]
  • On October 21, Re-us simulated a machine to halting.^[121]
• BB(4,3)
  • Andrew Ducharme reduced the number of holdouts from 4,720,332 to 4,719,315, a 0.02% reduction, by using enumerate.py.^[122]
• BB(2,5)
  • On October 2, prurq claimed to have used Aristotle AI, to prove one of the remaining holdouts halting, reducing the unofficial count to 38 out of initially 60 Rocq-proven.^[123]
  • On October 9, prurq simulated a machine to halting using a Rocq-certified program, reducing the official and unofficial counts to respectively 59 and 37.^[124]
  • On the same day, Andrew Ducharme released an unofficial holdout list of 37 machines.^[125]
  • On October 17, LegionMammal978 simulated 1RB---3RA2LA2RB_2LB3LA4LB4RA0RA (bbch) to over 10^{1,140,000,000} steps,^[126] previously claiming the machine to be a doubly-exponential probviously halting "hard-drive vampire".^[127][128]
• BB(2,6)
  • Andrew Ducharme reduced the number of holdouts from 412,086 to 389,503, a 5.48% reduction.^{[129][130][131]}
• BB(2,7)
  • Terry Ligocki enumerated 20K more subtasks, increasing the number of holdouts to 3,125,433,611. All 1 million subtasks have been enumerated! This enumeration took from November 2025 to October 2026 using the resources [Ligocki] had available to work on this enumeration. Now we can start decreasing the number of holdouts!

Cryptids

All Turing machines mentioned in this section work with an alphabet of 2 symbols unless explicitly stated. The bounds given also only consider Turing machines which work with 2 symbols.

• Cryptids in the Wild
  • On October 15, Google DeepMind claimed to have used Gemini 3.1 Pro to discover and prove simple rules that characterise the behavior of 11 BB(6) holdouts, noting them as potential Cryptids.^[132] Their methods are elaborated on in their paper, published this month.
• Larger Cryptids
  • Goldbach's Conjecture
    • On October 9, Google DeepMind claimed to have used Gemini 3.1 Pro to discover a 24-state proven to halt if and only if Goldbach's conjecture is false, improving on the previous smallest known machine with this property by one state.^[133]
    • On October 13, Google DeepMind claimed to have used Gemini 3.1 Pro to formally reduce the number of states required from 24 to 21.^[134]
  • Riemann Hypothesis
    • On October 10, Google DeepMind claimed to have used Gemini 3.1 Pro to formalize the claims of Shunia's 120-state TM's halting if and only if the Riemann hypothesis is false.^[135]
    • On October 13, Google DeepMind claimed to have used Gemini 3.1 Pro to formally reduce the number of states required for a specific TM to encode the truth value of the Riemann hypothesis from 120 to 104.^[136]
    • On October 19, Google DeepMind claimed to have used Gemini 3.1 Pro to formally reduce the bound from 104 states to 95 states.^[137]
  • Weak Collatz Conjecture
    • On October 18, Discord user charlie claimed to have used Claude to reduce the number of states required for a specific TM to encode the truth value of the Weak Collatz conjecture from 124 to 23.^[138]
    • On October 20, Mira claimed to have used GPT-6 Astra^[139] to reduce the number of states required from 23 to 16.^[140][141]
    • On the same day, charlie claimed to have used Claude to reduce this bound to 14 states.^[142][143]
  • Erdős Ternary Conjecture
    • On October 20, Tristan Stérin claimed to have used GPT-6 Astra^[144] to reduce the number of states required for a specific TM to encode the truth value of the Erdős ternary conjecture from 15 to 14.^[145]

      

  • Logical Independence
    • On October 6, Mira claimed to have used GPT-6 Astra to reduce their previous 256-state TM whose halting status is independent of ZFC, to a 254-state TM.^[146] They estimate that the Metamath formalization verifying that their previous 238-state TM is independent of Peano Arithmetic is roughly 70% complete, and the formalization verifying that their new 254-state ZFC-independent TM is roughly 40% complete.^[147]
    • On October 10, Google DeepMind claimed to have used Gemini 3.1 Pro to formalize the claims of the independence of Wade's 393-state TM's halting status from ZFC.^[148]
    • On October 13, Google DeepMind claimed to have used Gemini 3.1 Pro to formally reduce Andrew Wade's 393-state ZFC-independent TM, to a 380-state TM.^[149]
    • On the same day, Jeff Ketchersid claimed to have used Claude Opus 5.5 to formally reduce Andrew Wade's 393-state TM whose halting status is independent of ZFC, to a 335-state TM.^[150]
    • On October 14, Jeff Ketchersid claimed to have used Claude Opus 5.5 to prove the independence of Mira's 254-state TM's halting status from ZFC.^[151]
    • On October 15, Jeff Ketchersid claimed to have used Claude Opus 5.5 to discover a 296-state TM whose halting status is independent of ZFC + "Every set is contained in a Grothedieck universe".^[152]
    • On the same day, Mira claimed to have used GPT-6 Astra to prove the independence of their 238-state PA-independent TM, building off of Jeff Ketchersid's proof of their ZFC-independent TM.^[153]
    • On October 18, Vladimir Reshetnikov claimed to have used Claude to reduce Mira's previous 254-state ZFC-independent TM, to a 246-state TM.^[154][155]
    • On October 19, Kinata claimed to have used GPT-6 Astra^[156] to reduce Reshetnikov's previous 246-state ZFC-independent TM, to 230 states.^[157][158]
    • On October 20, Vladimir Reshetnikov claimed to have used Claude to optimize their previous 246-state, ZFC-independent TM, to 215 states.^[159]
  • Other Conjectures
    • On October 22, charlie claimed to have used Claude to provably encode the truth value of Fermat's Last Theorem in a specific 90-state TM, without relying on Andrew Wiles's proof^[160] of the theorem.^[161] This improves upon James Randels's 1965 construction (currently considered as a former Cryptid), which used (a maximum of) 400 states.
    • On October 23, roromachine14 claimed to have used Gemini 4 Argon to encode the truth value of a variant of the Erdős ternary conjecture in a 4-state, 4-symbol TM.^[162]

Misc

• On October 17, XnoobSpeakable began archiving messages of users who have consented to the archival project, as well as adding these archived messages to this wiki.^[163]