Cryptids - Revision history

Veljjanoski: Brocard row: machine reduced to 34 states (BB(34), BBi(66)); links updated

2026-11-09T07:41:17Z

Brocard row: machine reduced to 34 states (BB(34), BBi(66)); links updated

← Older revision		Revision as of 07:41, 9 November 2026
Line 368:		Line 368:
	\| '''Brocard'''		\| '''Brocard'''
	\| Halts iff [[wikipedia:Brocard's problem\|Brocard's problem]] <code>n! + 1 = m<sup>2</sup></code> has a solution with <code>n > 7</code>, i.e. beyond the known solutions <code>n = 4, 5, 7</code>.		\| Halts iff [[wikipedia:Brocard's problem\|Brocard's problem]] <code>n! + 1 = m<sup>2</sup></code> has a solution with <code>n > 7</code>, i.e. beyond the known solutions <code>n = 4, 5, 7</code>.
	\| '''BB(41)'''		\| '''BB(34)'''
	\| '''BBi(72)'''		\| '''BBi(66)'''
	\|[https://github.com/veljjanoski/cryptids/blob/brocard-41/artifacts/~~brocard_41~~/machine.txt Machine code]		\|[https://github.com/veljjanoski/cryptids/blob/brocard-41/artifacts/brocard_34/machine.txt Machine code]
	\|[https://github.com/veljjanoski/cryptids/tree/brocard-41/artifacts/~~brocard_41~~ GitHub] ([https://github.com/google-deepmind/cryptids/pull/27 PR to google-deepmind/cryptids])		\|[https://github.com/veljjanoski/cryptids/tree/brocard-41/artifacts/brocard_34 GitHub] ([https://github.com/google-deepmind/cryptids/pull/27 PR to google-deepmind/cryptids])
	\|style="white-space: nowrap; text-align: right;"\|Nov 2026		\|style="white-space: nowrap; text-align: right;"\|Nov 2026
	\|[https://www.linkedin.com/in/danielveljjanoski Daniel Veljjanoski]		\|[https://www.linkedin.com/in/danielveljjanoski Daniel Veljjanoski]
	\|Keeps <code>n!/8</code> in unary and tests it for triangularity (<code>n! + 1 = m<sup>2</sup></code> forces <code>m = 2k + 1</code>, <code>n!/8 = k(k+1)/2</code>). Includes a Lean formalization (kernel-checked; PR pending).<ref>https://github.com/veljjanoski/cryptids/blob/brocard-41/Cryptids/Semantics/~~Brocard41~~.lean</ref> An earlier 61-state machine with a Lean proof is by [[User:Frogmatic\|Charlie Reams]] ([https://github.com/calr3/tinycryptids/tree/main/brocard calr3 GitHub], Nov 2026); a 43-state table without a machine-checked proof is in [https://arxiv.org/abs/2605.20215 arXiv:2605.20215].		\|Keeps <code>n!/8</code> in unary and tests it for triangularity (<code>n! + 1 = m<sup>2</sup></code> forces <code>m = 2k + 1</code>, <code>n!/8 = k(k+1)/2</code>). Includes a Lean formalization (kernel-checked; PR pending).<ref>https://github.com/veljjanoski/cryptids/blob/brocard-41/Cryptids/Semantics/Brocard34.lean</ref> An earlier 61-state machine with a Lean proof is by [[User:Frogmatic\|Charlie Reams]] ([https://github.com/calr3/tinycryptids/tree/main/brocard calr3 GitHub], Nov 2026); a 43-state table without a machine-checked proof is in [https://arxiv.org/abs/2605.20215 arXiv:2605.20215].
	\|-		\|-
	\| '''Kurepa'''		\| '''Kurepa'''

Veljjanoski: Brocard row: link machine.txt instead of WrapTM (41 states exceed the 26-letter standard format; the bbchallenge viewer link rendered the machine wrongly)

2026-11-09T06:37:42Z

Brocard row: link machine.txt instead of WrapTM (41 states exceed the 26-letter standard format; the bbchallenge viewer link rendered the machine wrongly)

← Older revision		Revision as of 06:37, 9 November 2026
Line 370:		Line 370:
	\| '''BB(41)'''		\| '''BB(41)'''
	\| '''BBi(72)'''		\| '''BBi(72)'''
	\|~~{{WrapTM\|~~Machine code\|1LB---_1LC---_1LD---_0LE---_1LF---_1LG---_1LH---_1Rn---_0LJ1LI_1RK1LJ_0RR0RL_0RQ1RL_0RN1RM_1LO1RN_0LP1LO_1RQ1LP_0LI0RM_1RS1RR_0RT1LS_---0RU_0RV1RU_1LW1RV_0LX0LY_0Le1RU_0LZ1LY_1Ra1LZ_0Rb0RU_0Rc0Rb_0Ld0Rc_0Ld0LI_0Lf1Le_0Rn1Lg_0Rn1Lh_0Rn1Li_0Rn1Lj_0Rn1Lk_0Rn1Ll_0Rn1Lm_0Rn---_0Ro1Rn_1Rb1Ro\|undecided}}		\|[https://github.com/veljjanoski/cryptids/blob/brocard-41/artifacts/brocard_41/machine.txt Machine code]
	\|[https://github.com/veljjanoski/cryptids/tree/brocard-41/artifacts/brocard_41 GitHub] ([https://github.com/google-deepmind/cryptids/pull/27 PR to google-deepmind/cryptids])		\|[https://github.com/veljjanoski/cryptids/tree/brocard-41/artifacts/brocard_41 GitHub] ([https://github.com/google-deepmind/cryptids/pull/27 PR to google-deepmind/cryptids])
	\|style="white-space: nowrap; text-align: right;"\|Nov 2026		\|style="white-space: nowrap; text-align: right;"\|Nov 2026

Veljjanoski at 08:53, 7 November 2026

2026-11-07T08:53:14Z

@@ Line 365: / Line 365: @@
 |[[User:Frogmatic|Charlie Reams]]
 |Includes Lean formalization. Not independently verified.
 |-
 | '''Kurepa'''

Veljjanoski: →Larger Cryptids: Erdős Ternary BB(15) and BB(14) machines verified in Lean (google-deepmind/cryptids PR 19)

2026-11-06T18:47:45Z

→Larger Cryptids: Erdős Ternary BB(15) and BB(14) machines verified in Lean (google-deepmind/cryptids PR 19)

← Older revision		Revision as of 18:47, 6 November 2026
Line 287:		Line 287:
	\|style="white-space: nowrap; text-align: right;"\|Jul 2021		\|style="white-space: nowrap; text-align: right;"\|Jul 2021
	\| [[User:Cosmo\|Tristan Stérin]] (<code>@cosmo</code>) and Damien Woods		\| [[User:Cosmo\|Tristan Stérin]] (<code>@cosmo</code>) and Damien Woods
	\| Erdős #406 is the conjecture that "For all n > 8, there is at least one 2 in the base-3 representation of 2^n." [https://arxiv.org/abs/2107.12475 arxiv preprint]		\| Erdős #406 is the conjecture that "For all n > 8, there is at least one 2 in the base-3 representation of 2^n." [https://arxiv.org/abs/2107.12475 arxiv preprint]. The BB(15) machine's behavior has been verified in Lean.<ref>https://github.com/google-deepmind/cryptids/blob/main/Cryptids/Semantics/ErdosTernary15.lean</ref>
	\|-		\|-
	\| '''BB(14)'''		\| '''BB(14)'''
Line 295:		Line 295:
	\|style="white-space: nowrap; text-align: right;"\|Oct 2026		\|style="white-space: nowrap; text-align: right;"\|Oct 2026
	\|[[User:Cosmo\|Tristan Stérin]]		\|[[User:Cosmo\|Tristan Stérin]]
	\|~~Not independently~~ verified.		\|Its behavior has been verified in Lean.<ref>https://github.com/google-deepmind/cryptids/tree/main/artifacts/erdos_ternary_14</ref>
	\|-		\|-
	\| '''Erdős Ternary Conjecture''' variant		\| '''Erdős Ternary Conjecture''' variant

Polygon: /* Larger Cryptids */ fixed doubled name

2026-11-04T14:19:55Z

Larger Cryptids: fixed doubled name

← Older revision		Revision as of 14:19, 4 November 2026
Line 194:		Line 194:
	\|style="white-space: nowrap; text-align: right;"\|Oct 2026		\|style="white-space: nowrap; text-align: right;"\|Oct 2026
	\|[[wikipedia:Cleo (mathematician)\|Vladimir Reshetnikov]]		\|[[wikipedia:Cleo (mathematician)\|Vladimir Reshetnikov]]
	\|Machine-checked in Peano-Arithmetic by [https://github.com/elliotglazer/k215-pa ~~elliotglazer~~ Elliot Glazer].		\|Machine-checked in Peano-Arithmetic by [https://github.com/elliotglazer/k215-pa Elliot Glazer].
	\|-		\|-
	\|'''BB(152,9)'''		\|'''BB(152,9)'''

Loader3229: /* Larger Cryptids */

2026-11-04T08:05:30Z

Larger Cryptids

@@ Line 362: / Line 362: @@
 |[https://github.com/calr3/tinycryptids/blob/main/oddperfect/machines/oddperfect_37.txt Machine code]
 |[https://github.com/calr3/tinycryptids/tree/main/oddperfect calr3 GitHub]
 |style="white-space: nowrap; text-align: right;"|Oct 2026
 |[[User:Frogmatic|Charlie Reams]]

50 ft lock: Lambda term shown as the cryptid was 75 bits; changed it to the correct version

2026-11-02T05:50:48Z

Lambda term shown as the cryptid was 75 bits; changed it to the correct version

← Older revision		Revision as of 05:50, 2 November 2026
Line 583:		Line 583:
	\|		\|
	\|[[Lambda Calculus\|BBλ(74)]]		\|[[Lambda Calculus\|BBλ(74)]]
	\|<math>(\lambda1111(\lambda1)1(\~~lambda\lambda1~~))(\lambda\lambda\lambda1(322222))</math>		\|<math>(\lambda1111(\lambda1)1(\lambda2))(\lambda\lambda\lambda1(322222))</math>
	\|style="white-space: nowrap; text-align: right;"\|Apr 2025		\|style="white-space: nowrap; text-align: right;"\|Apr 2025
	\|50_ft_lock		\|50_ft_lock

Loader3229: /* Larger Cryptids */

2026-11-01T16:21:36Z

Larger Cryptids

← Older revision		Revision as of 16:21, 1 November 2026
Line 178:		Line 178:
	! Name !! Behaviour !! [[Busy Beaver Functions\|BB Domain]] !! [[Instruction-Limited Busy Beaver\|Instructions]] !! Machine !! Source !! Date !! Discoverer !! Note		! Name !! Behaviour !! [[Busy Beaver Functions\|BB Domain]] !! [[Instruction-Limited Busy Beaver\|Instructions]] !! Machine !! Source !! Date !! Discoverer !! Note
	\|-		\|-
	\|rowspan="2"\| '''[[Logical independence\|ZFC consistency]]'''		\|rowspan="3"\| '''[[Logical independence\|ZFC consistency]]'''
	\|rowspan="2"\| Halts iff [[wikipedia:Zermelo–Fraenkel_set_theory\|Zermelo–Fraenkel set theory]] with the Axiom of Choice is inconsistent.		\|rowspan="3"\| Halts iff [[wikipedia:Zermelo–Fraenkel_set_theory\|Zermelo–Fraenkel set theory]] with the Axiom of Choice is inconsistent.
	\|BB(432)		\|BB(432)
	\|		\|
Line 189:		Line 189:
	\|-		\|-
	\|'''BB(215)'''		\|'''BB(215)'''
	\|~~'''~~BBi(430)~~'''~~		\|BBi(430)
	\|[https://github.com/VladimirReshetnikov/ProveIt/blob/main/Computability/BusyBeaver/Research/ZFC/k225-formal/lean215/k215_k230labels.tm Machine code]		\|[https://github.com/VladimirReshetnikov/ProveIt/blob/main/Computability/BusyBeaver/Research/ZFC/k225-formal/lean215/k215_k230labels.tm Machine code]
	\|[https://github.com/VladimirReshetnikov/ProveIt/tree/main/Computability/BusyBeaver/Research/ZFC/k225-formal/verification/k215 VladimirReshetnikov on GitHub]		\|[https://github.com/VladimirReshetnikov/ProveIt/tree/main/Computability/BusyBeaver/Research/ZFC/k225-formal/verification/k215 VladimirReshetnikov on GitHub]
Line 195:		Line 195:
	\|[[wikipedia:Cleo (mathematician)\|Vladimir Reshetnikov]]		\|[[wikipedia:Cleo (mathematician)\|Vladimir Reshetnikov]]
	\|Machine-checked in Peano-Arithmetic by [https://github.com/elliotglazer/k215-pa elliotglazer Elliot Glazer].		\|Machine-checked in Peano-Arithmetic by [https://github.com/elliotglazer/k215-pa elliotglazer Elliot Glazer].
			\|-
			\|'''BB(152,9)'''
			'''BB(143,11)'''
			'''BB(117,12)'''
			\|'''BBi(376)'''
			\|
			\|[https://github.com/calr3/tinycryptids/tree/main/zfc_nsymbols calr3 GitHub]
			\|style="white-space: nowrap; text-align: right;"\|Nov 2026
			\|[[User:Frogmatic\|Charlie Reams]]
			\|Not independently verified.
	\|-		\|-
	\|'''Peano Arithmetic consistency'''		\|'''Peano Arithmetic consistency'''

Loader3229: /* Larger Cryptids */

2026-10-31T10:49:28Z

Larger Cryptids

← Older revision		Revision as of 10:49, 31 October 2026
Line 232:		Line 232:
	\|Not independently verified.		\|Not independently verified.
	\|-		\|-
	\| rowspan="2"\|'''Goldbach'''		\| rowspan="3"\|'''Goldbach'''
	\| rowspan="2"\|Halts iff [[wikipedia:Goldbach's conjecture\|Goldbach's conjecture]] is false		\| rowspan="3"\|Halts iff [[wikipedia:Goldbach's conjecture\|Goldbach's conjecture]] is false
	\|BB(25)		\|BB(25)
	\|BBi(49)		\|BBi(49)
Line 243:		Line 243:
	\|-		\|-
	\|'''BB(21)'''		\|'''BB(21)'''
	\|~~'''~~BBi(41)~~'''~~		\|BBi(41)
	\|{{WrapTM\|Machine code\|1LJ0RF_0RJ1RD_1RP1LC_---1RE_0LO1RG_1LQ1RF_0RH0LH_0LM1LU_1RB0LI_1RJ0RK_1RL1RK_0LM0LS_1LN1LM_1LO0LC_1LQ1LO_1RD1RP_0RA0LR_0RB1LR_1LT1LS_0LU0LI_0RB0LU\|undecided}}		\|{{WrapTM\|Machine code\|1LJ0RF_0RJ1RD_1RP1LC_---1RE_0LO1RG_1LQ1RF_0RH0LH_0LM1LU_1RB0LI_1RJ0RK_1RL1RK_0LM0LS_1LN1LM_1LO0LC_1LQ1LO_1RD1RP_0RA0LR_0RB1LR_1LT1LS_0LU0LI_0RB0LU\|undecided}}
	\|[https://github.com/google-deepmind/cryptids/tree/main/artifacts/goldbach_21 DeepMind GitHub]		\|[https://github.com/google-deepmind/cryptids/tree/main/artifacts/goldbach_21 DeepMind GitHub]
	\|style="white-space: nowrap; text-align: right;"\|Oct 2026		\|style="white-space: nowrap; text-align: right;"\|Oct 2026
	\|Google DeepMind		\|Google DeepMind
			\|Not independently verified.
			\|-
			\|'''BB(10,6)'''
			\|'''BBi(34)'''
			\|{{WrapTM\|Machine code\|1RD3LB---------5RF_0RD2RC2LB3LB---5RD_0LE2LB2RC3RC2LB5LE_1LD1LI1RD3LB------_0RH1RE1LE4LE1RA1LI_---1RG------------_---1RA------------_---1RH------1RH1LI_1RF5LJ------------_0RF1LJ---------1LJ\|undecided}}
			\|[https://github.com/calr3/tinycryptids/tree/main/goldbach calr3 GitHub]
			\|style="white-space: nowrap; text-align: right;"\|Oct 2026
			\|[[User:Frogmatic\|Charlie Reams]]
	\|Not independently verified.		\|Not independently verified.
	\|-		\|-

Frogmatic: /* Cryptids for other BB-style functions */ Split behavior out from other notes for BBB, consistent with the BB table.

2026-10-31T09:29:52Z

Cryptids for other BB-style functions: Split behavior out from other notes for BBB, consistent with the BB table.

← Older revision		Revision as of 09:29, 31 October 2026
Line 418:		Line 418:
	{\| class="wikitable"		{\| class="wikitable"
	\|-		\|-
	! Name !! BBB domain !! Machine !! Source !! Date !! Discoverer !! Note		! Name !! Behaviour !! BBB domain !! Machine !! Source !! Date !! Discoverer !! Note
	\|-		\|-
	\|[[Mother of Giants]]		\|[[Mother of Giants]]
			\|Probviously quasihalting.
	\|[[Beeping Busy Beaver\|BBB(5)]]		\|[[Beeping Busy Beaver\|BBB(5)]]
	\|{{WrapTM\|Machine code\|1RB1LE_0LC0LB_0LD1LC_1RD1RA_1RC0LA\|non_halt}} and 3 others		\|{{WrapTM\|Machine code\|1RB1LE_0LC0LB_0LD1LC_1RD1RA_1RC0LA\|non_halt}} and 3 others
Line 426:		Line 427:
	\|style="white-space: nowrap; text-align: right;"\|Apr 2022		\|style="white-space: nowrap; text-align: right;"\|Apr 2022
	\|[[User:Sligocki\|Shawn Ligocki]]		\|[[User:Sligocki\|Shawn Ligocki]]
	\|~~Probviously quasihalting.~~		\|
	\|-		\|-
	\|Fermat Primes		\|Fermat Primes
			\|Quasihalts iff there are only finitely many Fermat primes.
	\|[[Beeping Busy Beaver\|BBB(16)]]		\|[[Beeping Busy Beaver\|BBB(16)]]
	\|{{WrapTM\|Machine code (beep state: P)\|1LO1LA_0LI0LC_0LD1LC_1RE1LD_0LF0RG_0RE1LF_0RH1RG_1RB1RH_---0LJ_1LK1LJ_1RA0LL_0LM0LL_0RN1RO_1RN1LA_1RO1RP_0LA0RB\|non_halt}}		\|{{WrapTM\|Machine code (beep state: P)\|1LO1LA_0LI0LC_0LD1LC_1RE1LD_0LF0RG_0RE1LF_0RH1RG_1RB1RH_---0LJ_1LK1LJ_1RA0LL_0LM0LL_0RN1RO_1RN1LA_1RO1RP_0LA0RB\|non_halt}}
Line 434:		Line 436:
	\|style="white-space: nowrap; text-align: right;"\|Oct 2026		\|style="white-space: nowrap; text-align: right;"\|Oct 2026
	\|[[User:Frogmatic\|Charlie Reams]]		\|[[User:Frogmatic\|Charlie Reams]]
	\|~~The machine [[quasihalt]]s if and only if there are only finitely many Fermat primes.~~ Not independently verified.		\|Not independently verified.
	\|-		\|-
	\|[[wikipedia:Twin prime#Twin_prime_conjecture\|Twin prime conjecture]]		\|[[wikipedia:Twin prime#Twin_prime_conjecture\|Twin prime conjecture]]
			\|Quasihalts iff Twin Prime conjecture is false.
	\|[[Beeping Busy Beaver\|BBB(18)]]		\|[[Beeping Busy Beaver\|BBB(18)]]
	\|{{WrapTM\|Machine code (beep state: N)\|1LB1RA_0LH0LC_0LD1LC_1RE1LD_0LF0RG_0RE1LF_0RA1RG_1RP1LI_1RL1LJ_1RP1LK_1RL1LK_0RM1RL_---0RN_0LB1RO_0LB1RO_1LQ1RP_1RR1LQ_---0RM\|non_halt}}		\|{{WrapTM\|Machine code (beep state: N)\|1LB1RA_0LH0LC_0LD1LC_1RE1LD_0LF0RG_0RE1LF_0RA1RG_1RP1LI_1RL1LJ_1RP1LK_1RL1LK_0RM1RL_---0RN_0LB1RO_0LB1RO_1LQ1RP_1RR1LQ_---0RM\|non_halt}}
Line 442:		Line 445:
	\|style="white-space: nowrap; text-align: right;"\|Oct 2026		\|style="white-space: nowrap; text-align: right;"\|Oct 2026
	\|[[User:Frogmatic\|Charlie Reams]]		\|[[User:Frogmatic\|Charlie Reams]]
	\|~~The machine [[quasihalt]]s if and only if Twin Prime conjecture is false.~~ Not independently verified.		\|Not independently verified.
	\|-		\|-
	\|Collatz		\|Collatz
			\|Quasihalts iff the [[wikipedia:Collatz conjecture\|Collatz conjecture]] is false.
	\|[[Beeping Busy Beaver\|BBB(17)]]		\|[[Beeping Busy Beaver\|BBB(17)]]
	\|{{WrapTM\|Machine code (beep state: O)\|1RL0RB_1LC1RB_0LK0LD_1RE1LD_0RF0RB_0LG0LG_1LH1LG_0RA0RI_1RJ1RI_1RF1RF_0RA1LK_0LM0LM_0LN1LM_1RO1LN_0RA0RP_0RQ1RP_1RL1RQ\|non_halt}}		\|{{WrapTM\|Machine code (beep state: O)\|1RL0RB_1LC1RB_0LK0LD_1RE1LD_0RF0RB_0LG0LG_1LH1LG_0RA0RI_1RJ1RI_1RF1RF_0RA1LK_0LM0LM_0LN1LM_1RO1LN_0RA0RP_0RQ1RP_1RL1RQ\|non_halt}}
Line 450:		Line 454:
	\|style="white-space: nowrap; text-align: right;"\|Oct 2026		\|style="white-space: nowrap; text-align: right;"\|Oct 2026
	\|[https://github.com/Mira-Cult Mira Cult]		\|[https://github.com/Mira-Cult Mira Cult]
	\|~~The machine [[quasihalt]]s if and only if the full [[wikipedia:Collatz conjecture\|Collatz conjecture]] is false.~~ Not independently verified.		\|Not independently verified.
	\|}		\|}