TMBR: November 2026: Difference between revisions
Jump to navigation
Jump to search
→Champions: Updated BB(6,6) |
Loader3229 (talk | contribs) |
||
| (15 intermediate revisions by 7 users not shown) | |||
| Line 2: | Line 2: | ||
[[:Category:This Month in Beaver Research|This Month in Beaver Research]] for November 2026. | [[:Category:This Month in Beaver Research|This Month in Beaver Research]] for November 2026. | ||
== Media == | |||
* YouTube video: [https://www.youtube.com/watch?v=pZrjqwlYbF0 Skelet #17: The Last Obstacle to solving Busy Beaver 5]. NLogSpace. 6 Nov 2026. | |||
== BB Adjacent == | == BB Adjacent == | ||
| Line 16: | Line 20: | ||
!Discoverer | !Discoverer | ||
!Previous''' '''lower''' '''bound | !Previous''' '''lower''' '''bound | ||
|- | |||
|BB(17) | |||
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RZ1LO|halt}} | |||
| rowspan="2" |Jeff Ketchersid | |||
|<math>f_{\omega + 3}^3(9)</math> | |||
|- | |||
|BB(18) | |||
|{{TM|1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RR0LO_0RO1RZ|halt}} | |||
|<math>f_{\omega + 3}^4(9)</math> | |||
|Jeff Ketchersid | |||
|<math>f_{\omega + 3}(114)</math> | |||
|- | |||
|BB(19) | |||
|{{TM|1RQ1RL_0LI1RC_0LD1LF_0RA1LD_1RB1RE_1LH0LG_1LF1LG_1RE1RM_1LJ1LI_0LK1LI_1RL1RA_0RL0RE_0LN1RM_1LO0LO_1RE1LP_1LN1LN_1LR1RQ_1RZ1LS_0LE0LR|halt}} | |||
| rowspan="2" |[[User:Jacobzheng]] | |||
|<math>f_{\omega + 7}^2(5)</math> | |||
|- | |- | ||
|BB(20) | |BB(20) | ||
|{{TM| | |{{TM|1LH0LG_0LI1RC_0LD1LA_0RE1LD_1RQ1RL_1RB1RF_1LA1LG_1RF1RM_1LJ1LI_0LK1LI_1RL1RE_0RL0RF_0LN1RM_0RF0LO_0RF1LP_0RF1LN_1LR1RQ_1RZ1LS_0LF1LT_0LF0LR|halt}} | ||
|<math>f_{\omega * 2}(f_{\omega + 2}^2(f_{10}(2)))</math> | |||
|<math>f_{\omega + | |||
| rowspan="2" |[[User:Jacobzheng]] | | rowspan="2" |[[User:Jacobzheng]] | ||
|<math>f_{\omega + 6}^2(4)</math> | |<math>f_{\omega + 6}^2(4)</math> | ||
| Line 26: | Line 45: | ||
|BB(11,4) | |BB(11,4) | ||
|{{TM|1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK|halt}} | |{{TM|1RG3LB1RZ2RA_2LD---1LD2RA_3RB1LB3LC2RC_3RE---3LC2RC_---3RE3LH2LF_3RF2RF2LE1LF_2LC3LH2LJ2RG_---3RH1LI2RG_3RH1LH3LI2RI_------3LJ3RK_------2RA3RK|halt}} | ||
| rowspan=" | | rowspan="9" |[[User:Loader3229]] | ||
|<math>f_{\omega \cdot 2}(21)</math> | |<math>f_{\omega \cdot 2}(21)</math> | ||
|<math>f_{\omega + 3}^2(4)</math> | |<math>f_{\omega + 3}^2(4)</math> | ||
| Line 50: | Line 69: | ||
|- | |- | ||
|BB(7,6) | |BB(7,6) | ||
|{{TM| | |{{TM|2LE3LB1RZ2RA4LB2LD_0LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE0LG4LC3LG5LE_5RB5RB---1LF---5LF_5LF---3RC1LG---5LG|halt}} | ||
|<math>f_{\omega^2}( | |<math>f_{\omega^2}(63)</math> | ||
|- | |||
|BB(8,6) | |||
|{{TM|0LC3LB2LH2RA4LB1RZ_3LH3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC2LD3RD_5RB3RE---4LC3LG5LE_5RB5RB---1LF5LF5LF_5LF4RG1LB1LG5LD5LG_3LE---1LH1LH---5RG|halt}} | |||
|<math>f_{\omega^2 + 1}(7)</math> | |||
|- | |||
|BB(3,7) | |||
|{{TM|6LC3LB5RA2RA4LB2LA5LC_1RZ3RB1LC2RA3RB4LC0LA_3RB1LB3LC2RC4LC5LC---|halt}} | |||
|<math>f_{\omega + 1}(77)</math> | |||
|[[User:Loader3229]] | |||
|<math>f_{\omega}^4(15)</math> | |||
|- | |||
|BB(4,7) | |||
|{{TM|6LD3LB5LD2RA4LB3LC5LA_1RZ3RB1LC2RA3RD---2RA_3RB1LB3LC2RC4LC3LC5LD_3RB---6LC4LD4LC4LD---|halt}} | |||
|<math>f_{\omega + 2}(124)</math> | |||
|} | |} | ||
* [[User:Loader3229]] discovered an array of champions based on Kropitz's current [[BB(3,4)]] champion, demonstrating the following bounds: | * [[User:Loader3229]] discovered an array of champions based on Kropitz's current [[BB(3,4)]] champion and Jacobzheng's former BB(11,3) champion, demonstrating the following bounds: | ||
** On November 1, BB(8,5) > <math>f_{\omega \cdot 2 + 1}(93)</math>.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1566410612949385317]</sup> and BB(11,4) > <math>f_{\omega \cdot 2}(21)</math>.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1566423230187700245]</sup> | ** On November 1, BB(8,5) > <math>f_{\omega \cdot 2 + 1}(93)</math>.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1566410612949385317]</sup> and BB(11,4) > <math>f_{\omega \cdot 2}(21)</math>.<sup>[https://discord.com/channels/960643023006490684/1084047886494470185/1566423230187700245]</sup> | ||
** On November 2, BB(4,6) > <math>f_{\omega + 2}(29)</math>, BB(5,6) > <math>f_{\omega + 3}(31)</math>, BB(6,6) > <math>f_{\omega | ** On November 2, BB(4,6) > <math>f_{\omega + 2}(29)</math>, BB(5,6) > <math>f_{\omega + 3}(31)</math>, BB(6,6) > <math>f_{\omega \times 2}(36)</math> and BB(7,6) > <math>f_{\omega^2}(28)</math>. | ||
** On November 3, BB(6,6) > <math>f_{\omega * 2}(89)</math>. | ** On November 3, BB(6,6) > <math>f_{\omega * 2}(89)</math>. | ||
* On November 2, [[User:Jacobzheng]] discovered | ** On November 4, BB(7,6) > <math>f_{\omega^2}(63)</math>, BB(8,6) > <math>f_{\omega^2 + 1}(7)</math>, BB(3,7) > <math>f_{\omega + 1}(77)</math> and BB(4,7) > <math>f_{\omega + 2}(124)</math> | ||
* [[User:Jacobzheng]] discovered the following bounds: | |||
** On November 2, BB(20) > <math>f_{\omega + 7}^2(5)</math>. | |||
** On November 4, BB(19) > <math>f_{\omega + 7}^2(5)</math> and BB(20) > <math>f_{\omega \times 2}(f_{\omega + 2}^2(f_{10}(2))</math>. | |||
* On November 4, Jeff Ketchersid used Claude and Gemini to discover the bounds BB(17) > <math>f_{\omega + 3}(9)</math>, BB(18) > <math>f_{\omega + 3}^4(9)</math> and BB(19) > <math>f_{\omega + 4}(f_{\omega + 2}(114))</math>. | |||
== Holdouts == | == Holdouts == | ||
| Line 98: | Line 135: | ||
*** [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo-Frankel set theory]] | *** [[wikipedia:Zermelo–Fraenkel_set_theory|Zermelo-Frankel set theory]] | ||
**** On November 1, charlie claimed to have used Claude to [https://github.com/calr3/tinycryptids/tree/main/zfc_nsymbols/mm0 formally] reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition). | **** On November 1, charlie claimed to have used Claude to [https://github.com/calr3/tinycryptids/tree/main/zfc_nsymbols/mm0 formally] reduce the number of defined instructions required in a ZFC-independent TM to 375 (376 including the halting transition). | ||
** Computational Complexity Theory | ***[[wikipedia:New_foundations|New Foundations]] | ||
****On November 6, svennik-alt-account used ChatGPT 6 Astra to find a 210-state TM that halts iff New Foundations is inconsistent. This is accompanied by a Lean proof. This is also the smallest known TM which PA cannot prove is non-halting. | |||
=== Computational Complexity Theory === | |||
* On November 1, [[User:GregoryMorse|GregoryMorse]] announced 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.<ref name="GregoryMorseNov1">https://discord.com/channels/960643023006490684/1385498968011575366/1566326998563823719</ref> | |||
* On November 4, [https://github.com/Mira-Cult Mira-Cult] announced a Lean formalization of a 285-state P = NP beeper. | |||
* On November 6, [https://github.com/Mira-Cult Mira-Cult] released proofs for 284-state and 266-state NP = coNP beepers; the 284-state table is Lean-formalized, while the 266-state construction has a conventional proof. | |||
* On November 9, [[User:GregoryMorse|GregoryMorse]] completed Lean formalizations for a suite of ten beepers, constructed with Claude assistance. These use designated beep states; Mira-Cult's headline counts use designated beep transitions. | |||
{| class="wikitable" | |||
! Problem !! Domain / convention !! Discoverer !! Date !! Proof and notes | |||
|- | |||
| P = NP | |||
| [[Beeping Busy Beaver|BBB(285)]] (beep transition) | |||
| [https://github.com/Mira-Cult Mira-Cult] | |||
| November 4 | |||
| [https://github.com/Mira-Cult/math/blob/main/turing-machines/p-equals-np-285/formalization/Shared/PNP/Record285/PublicEndpoint.lean Lean proof]; 286-state beep-state companion also formalized. | |||
|- | |||
| NP = coNP | |||
| [[Beeping Busy Beaver|BBB(284)]] (beep transition) | |||
| [https://github.com/Mira-Cult Mira-Cult] | |||
| November 6 | |||
| [https://github.com/Mira-Cult/math/blob/main/turing-machines/np-equals-conp/beeper284/formalization/Shared/Beeping/NPcoNP/Bootstrap284AlignedFromBlank.lean Lean proof]; 285-state state-exit companion documented. | |||
|- | |||
| NP = coNP | |||
| [[Beeping Busy Beaver|BBB(266)]] (beep transition) | |||
| [https://github.com/Mira-Cult Mira-Cult] | |||
| November 6 | |||
| [https://github.com/Mira-Cult/math/blob/main/turing-machines/np-equals-conp/beeper266/PROOF.md Conventional proof]; 267-state state-exit companion documented. | |||
|- | |||
| P = NP | |||
| [[Beeping Busy Beaver|BBB(278)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/Solution.lean Lean proof] and [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/Hard.lean NP-completeness proof]. | |||
|- | |||
| P = PSPACE | |||
| [[Beeping Busy Beaver|BBB(291)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainPS.lean Lean proof]: alternating-quantifier language in P. | |||
|- | |||
| P = PP | |||
| [[Beeping Busy Beaver|BBB(295)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainPP.lean Lean proof]: majority-acceptance language in P. | |||
|- | |||
| NP = coNP | |||
| [[Beeping Busy Beaver|BBB(317)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainConp.lean Lean proof]: polynomially clocked nondeterministic verifier for the reference language's complement. | |||
|- | |||
| Integer factorization in P | |||
| [[Beeping Busy Beaver|BBB(324)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainF.lean Lean proof]: bounded-divisor decision language in P. | |||
|- | |||
| Discrete logarithms modulo primes in P | |||
| [[Beeping Busy Beaver|BBB(400)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainD.lean Lean proof]: bounded-exponent decision language in P. | |||
|- | |||
| Linear-time multiplication | |||
| [[Beeping Busy Beaver|BBB(403)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainMul.lean Lean proof]: linear time in the queue-of-stacks model. | |||
|- | |||
| Graph isomorphism in P | |||
| [[Beeping Busy Beaver|BBB(415)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainG.lean Lean proof]: graph-isomorphism decision language in P. | |||
|- | |||
| Linear-size NTT circuits | |||
| [[Beeping Busy Beaver|BBB(469)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainNTT.lean Lean proof]: chain-circuit condition. | |||
|- | |||
| Twin prime conjecture | |||
| [[Beeping Busy Beaver|BBB(19)]] (beep state) | |||
| [[User:GregoryMorse|GregoryMorse]], Claude | |||
| November 9 | |||
| [https://github.com/GregoryMorse/NP-complete/blob/main/formal/ZP/MainTwin.lean Lean proof]; quasihalts iff the conjecture is false. | |||
|} | |||
{| class="wikitable" | {| class="wikitable" | ||
| Line 115: | Line 242: | ||
|Unknown - pseudoquasihalts if the conjecture is false. [https://github.com/calr3/tinycryptids/tree/main/lean/TinyCryptids/Pillai Proof.] | |Unknown - pseudoquasihalts if the conjecture is false. [https://github.com/calr3/tinycryptids/tree/main/lean/TinyCryptids/Pillai Proof.] | ||
|} | |} | ||
[[Category:This Month in Beaver Research]] | [[Category:This Month in Beaver Research|2026-11]] | ||
Latest revision as of 12:11, 10 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.
Media
- YouTube video: Skelet #17: The Last Obstacle to solving Busy Beaver 5. NLogSpace. 6 Nov 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(17) | 1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RZ1LO (bbch)
|
Jeff Ketchersid | |||
| BB(18) | 1LB1LA_1RC0LA_1RD1RC_1RE1RK_1RF0LJ_1LG1RI_1RM0LM_1LG0RC_0RN0LE_1LA1LE_0LL1LB_0RM1LL_1LF1RH_1RQ0LO_1LP1LN_0RB1LI_1RR0LO_0RO1RZ (bbch)
|
Jeff Ketchersid | |||
| BB(19) | 1RQ1RL_0LI1RC_0LD1LF_0RA1LD_1RB1RE_1LH0LG_1LF1LG_1RE1RM_1LJ1LI_0LK1LI_1RL1RA_0RL0RE_0LN1RM_1LO0LO_1RE1LP_1LN1LN_1LR1RQ_1RZ1LS_0LE0LR (bbch)
|
User:Jacobzheng | |||
| BB(20) | 1LH0LG_0LI1RC_0LD1LA_0RE1LD_1RQ1RL_1RB1RF_1LA1LG_1RF1RM_1LJ1LI_0LK1LI_1RL1RE_0RL0RF_0LN1RM_0RF0LO_0RF1LP_0RF1LN_1LR1RQ_1RZ1LS_0LF1LT_0LF0LR (bbch)
|
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) | 4LF3LB1RZ2RA4LB---_2LC3RB1LD2RA3LF---_3RB1LB3LC2RC4LC0LE_3RB---3LC2RC---3RE_5RC3RE---4LC------_5RB0LF1RB1LF---5RB (bbch)
|
||||
| BB(7,6) | 2LE3LB1RZ2RA4LB2LD_0LA3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC---3RD_5RB3RE0LG4LC3LG5LE_5RB5RB---1LF---5LF_5LF---3RC1LG---5LG (bbch)
|
||||
| BB(8,6) | 0LC3LB2LH2RA4LB1RZ_3LH3RB1LD2RA3LF5RB_3RB1LB3LC2RC4LC1LE_3RB3RE3LC2RC2LD3RD_5RB3RE---4LC3LG5LE_5RB5RB---1LF5LF5LF_5LF4RG1LB1LG5LD5LG_3LE---1LH1LH---5RG (bbch)
|
||||
| BB(3,7) | 6LC3LB5RA2RA4LB2LA5LC_1RZ3RB1LC2RA3RB4LC0LA_3RB1LB3LC2RC4LC5LC--- (bbch)
|
User:Loader3229 | |||
| BB(4,7) | 6LD3LB5LD2RA4LB3LC5LA_1RZ3RB1LC2RA3RD---2RA_3RB1LB3LC2RC4LC3LC5LD_3RB---6LC4LD4LC4LD--- (bbch)
|
- User:Loader3229 discovered an array of champions based on Kropitz's current BB(3,4) champion and Jacobzheng's former BB(11,3) champion, demonstrating the following bounds:
- User:Jacobzheng discovered the following bounds:
- On November 2, BB(20) > .
- On November 4, BB(19) > and BB(20) > .
- On November 4, Jeff Ketchersid used Claude and Gemini to discover the bounds BB(17) > , BB(18) > and BB(19) > .
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).
- New Foundations
- On November 6, svennik-alt-account used ChatGPT 6 Astra to find a 210-state TM that halts iff New Foundations is inconsistent. This is accompanied by a Lean proof. This is also the smallest known TM which PA cannot prove is non-halting.
- Zermelo-Frankel set theory
- Logical Independence
Computational Complexity Theory
- On November 1, GregoryMorse announced 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.[1]
- On November 4, Mira-Cult announced a Lean formalization of a 285-state P = NP beeper.
- On November 6, Mira-Cult released proofs for 284-state and 266-state NP = coNP beepers; the 284-state table is Lean-formalized, while the 266-state construction has a conventional proof.
- On November 9, GregoryMorse completed Lean formalizations for a suite of ten beepers, constructed with Claude assistance. These use designated beep states; Mira-Cult's headline counts use designated beep transitions.
| Problem | Domain / convention | Discoverer | Date | Proof and notes |
|---|---|---|---|---|
| P = NP | BBB(285) (beep transition) | Mira-Cult | November 4 | Lean proof; 286-state beep-state companion also formalized. |
| NP = coNP | BBB(284) (beep transition) | Mira-Cult | November 6 | Lean proof; 285-state state-exit companion documented. |
| NP = coNP | BBB(266) (beep transition) | Mira-Cult | November 6 | Conventional proof; 267-state state-exit companion documented. |
| P = NP | BBB(278) (beep state) | GregoryMorse, Claude | November 9 | Lean proof and NP-completeness proof. |
| P = PSPACE | BBB(291) (beep state) | GregoryMorse, Claude | November 9 | Lean proof: alternating-quantifier language in P. |
| P = PP | BBB(295) (beep state) | GregoryMorse, Claude | November 9 | Lean proof: majority-acceptance language in P. |
| NP = coNP | BBB(317) (beep state) | GregoryMorse, Claude | November 9 | Lean proof: polynomially clocked nondeterministic verifier for the reference language's complement. |
| Integer factorization in P | BBB(324) (beep state) | GregoryMorse, Claude | November 9 | Lean proof: bounded-divisor decision language in P. |
| Discrete logarithms modulo primes in P | BBB(400) (beep state) | GregoryMorse, Claude | November 9 | Lean proof: bounded-exponent decision language in P. |
| Linear-time multiplication | BBB(403) (beep state) | GregoryMorse, Claude | November 9 | Lean proof: linear time in the queue-of-stacks model. |
| Graph isomorphism in P | BBB(415) (beep state) | GregoryMorse, Claude | November 9 | Lean proof: graph-isomorphism decision language in P. |
| Linear-size NTT circuits | BBB(469) (beep state) | GregoryMorse, Claude | November 9 | Lean proof: chain-circuit condition. |
| Twin prime conjecture | BBB(19) (beep state) | GregoryMorse, Claude | November 9 | Lean proof; quasihalts iff the conjecture is false. |
| Conjecture | Domain | Discoverer | Discovery date | Notes |
|---|---|---|---|---|
| Pillai's conjecture | BBBB(91) | charlie, Claude[6] | November 1 | Unknown - pseudoquasihalts if the conjecture is false. Proof. |