Cryptids

Lovecraftian Beaver fan art made by Lauren

Cryptids are Turing Machines whose behavior (when started on a blank tape) can be described completely by a relatively simple mathematical rule, but where that rule falls into a class of unsolved (and presumed hard) mathematical problems. This definition is somewhat subjective (What counts as a simple rule? What counts as a hard problem?). In practice, most currently known small Cryptids have Collatz-like behavior. In other words, the halting problem from blank tape of Cryptids is mathematically-hard.

If there exists a Cryptid with n states and m symbols, then BB(n, m) cannot be solved without solving this hard math problem.

The name Cryptid was proposed by Shawn Ligocki in an Oct 2023 blog post announcing the discovery of Bigfoot.

Cryptids at the Edge

This is a list of notable Minimal Cryptids (Cryptids in a domain with no strictly smaller known Cryptid). All of these Cryptids were "discovered in the wild" rather than "constructed".

Name	BB/BBi domain	Machine	Date	Discoverer	Note
Bigfoot	BB(3,3) BBi(8)	1RB2RA1LC_2LC1RB2RB_---2LA1LA (bbch)	Nov 2023	Shawn Ligocki	Probviously non-halting.
Hydra	BB(2,5) BBi(9)	1RB3RB---3LA1RA_2LA3RA4LB0LB0LA (bbch)	May 2024	Daniel Yuan	Probviously non-halting.
Bonus cryptid	BB(2,5) BBi(9)	1RB3RB---3LA1RA_2LA3RA4LB0LB1LB (bbch)	May 2024	Daniel Yuan	Probviously non-halting.
Antihydra	BB(6)	1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA (bbch)	Jun 2024	mxdys, shown to be a Cryptid by Racheline.	Same as Hydra but starting iteration from 8 instead of 3 and with termination condition O > 2E instead of E > 2O, hence the name Antihydra.
Lucy's Moonlight	BB(6)	1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA (bbch)	Mar 2025	Racheline	Probviously halting.
	BB(6)	1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA (bbch)	Jul 2024	mxdys	Variant of Hydra and Antihydra. Probviously non-halting.
	BB(6)	1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC (bbch)	Aug 2024	mxdys	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting.
	BB(6)	1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB--- (bbch)	Sep 2024	Daniel Yuan	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting.
	BB(6)	1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB (bbch)	Nov 2024	Racheline	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting.
Space Needle	BB(6)	1RB1LA_1LC0RE_1LF1LD_0RB0LA_1RC1RE_---0LD (bbch)	Jan 2025	mxdys	Probviously non-halting.
	BB(6)	1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC (bbch)	Jul 2024	mxdys	Has near-identical behavior to 16 related BB(6) holdouts. Probviously halting.
	BB(6)	1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF (bbch)	Jul 2024	Racheline	Probviously halting.
	BB(6)	1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB (bbch)	Jul 2024	Racheline	Probviously halting.
	BB(6)	1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA (bbch)	Jul 2024	Racheline	Probviously halting.
	BB(6)	1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE (bbch)	Nov 2024	Racheline	Probviously halting.
	BB(6)	1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA (bbch)	Nov 2024	Racheline	Probviously halting.
	BB(6)	1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE (bbch)	Jul 2025	mxdys	Probviously halting.
	BB(6)	1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE (bbch)	Jul 2024	Racheline	Probviously decidable. Estimated to have a 3/5 chance of becoming a translated cycler and a 2/5 chance of halting.
	BB(6)	1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC (bbch)	Aug 2024	mxdys, shown to be a Cryptid by DrDisentangle	Similar to Space Needle, probviously non-halting.
	BB(6)	1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE (bbch)	Apr 2026	sheep, shown to be a Cryptid by Daniel Yuan	Similar to Space Needle, probviously non-halting.
	BB(6)	1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB (bbch)	Feb 2025	Racheline	Probviously halting.

The following machines have chaotic behavior, but have not been classified as Cryptids due to seemingly lacking a connection to any known open mathematical problems, such as Collatz-like problems.

• 1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE (bbch)
• 1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE (bbch)
• 1RB---0RB0LA2RA_2LB2LA3RA4LB0LB (bbch)
• 1RB3LA1LA1RA3RA_2LB2RA---4RB1LB (bbch)
• 1RB3LA1LA1RA1RA_2LB2RA---4RB1LB (bbch)
• 1RB3LB---4LA1RB_2LA4LA4LB3RB1RA (bbch) Analysis by @mxdys

Larger Cryptids

A more complete list of notable known Cryptids over a wider range of states and symbols. These Cryptids were all "constructed" rather than "discovered". The best known bounds for each problem (with respect to BB(...), BB(..., n), and BBi(...)) are shown in bold.

Name	Behaviour	BB Domain	Instructions	Machine	Source	Date	Discoverer	Note
ZFC consistency	Halts iff Zermelo–Fraenkel set theory with the Axiom of Choice is inconsistent.	BB(432)		Wade's machine	ajwade on codeberg.org	Aug 2025	Wade, based on work by CatIsFluffy and O'Rear	This also covers ZFC.
		BB(215)	BBi(430)	Machine code	VladimirReshetnikov on GitHub	Oct 2026	Vladimir Reshetnikov	Machine-checked in Peano-Arithmetic by Elliot Glazer.
		BB(152,9) BB(143,11) BB(117,12)	BBi(376)		calr3 GitHub	Nov 2026	Charlie Reams	Not independently verified.
Peano Arithmetic consistency	Halts iff Peano arithmetic is inconsistent.	BB(372)	BBi(742)		LegionMammal978 GitHub	2026	LegionMammal	Discord announcement
Riemann Hypothesis	Halts iff the Riemann hypothesis is false.	BB(744)		Machine code	metamath-turing-machines GitHub	2016	Matiyasevich and O’Rear
		BB(120)	BBi(238)	Machine code	arxiv	Sep 2026	Joseph M. Shunia
		BB(95)	BBi(189)	Machine code	DeepMind GitHub	Oct 2026	Google DeepMind	Not independently verified.
Goldbach	Halts iff Goldbach's conjecture is false	BB(25)	BBi(49)	Machine code 1RB1RD_1LC1RB_0RA1LC_0LQ1RE_0LF1RG_0LC1LF_0LF0LH_1LQ1LI_0RJ0LI_1RK0LJ_0RL0RS_1RL0RM_1RN1RM_0LO0LU_0LP1LO_1RH1LX_1LR1LQ_0RK0LT_1LR1RS_---1RC_1LV1LU_0LW0LJ_0RK0LW_1RY1LX_1RE1RY (bbch)	GitHub	May 2016	anonymous	Its behavior has been verified in Lean.
		BB(21)	BBi(41)	Machine code 1LJ0RF_0RJ1RD_1RP1LC_---1RE_0LO1RG_1LQ1RF_0RH0LH_0LM1LU_1RB0LI_1RJ0RK_1RL1RK_0LM0LS_1LN1LM_1LO0LC_1LQ1LO_1RD1RP_0RA0LR_0RB1LR_1LT1LS_0LU0LI_0RB0LU (bbch)	DeepMind GitHub	Oct 2026	Google DeepMind	Not independently verified.
		BB(10,6)	BBi(34)	Machine code 1RD3LB---------5RF_0RD2RC2LB3LB---5RD_0LE2LB2RC3RC2LB5LE_1LD1LI1RD3LB------_0RH1RE1LE4LE1RA1LI_---1RG------------_---1RA------------_---1RH------1RH1LI_1RF5LJ------------_0RF1LJ---------1LJ (bbch)	calr3 GitHub	Oct 2026	Charlie Reams	Not independently verified.
Fermat prime	Halts if and only if there is a Fermat prime greater than 65537.	BB(25)	BBi(44)	Machine code 1LB---_1LC---_1LD---_1LE---_1LF---_1LG0LO_0LY0RM_0LF0LI_0LJ1LI_1RK1LJ_0LL0RM_0RG1LL_0RN1RM_1RH1RN_1LP1LO_1RY0LQ_0LR0LQ_0RS1RT_1RS1LY_1RT1RU_0RV0RH_0RV0RW_0LZ1LX_0LX1LY_1LT1LY (bbch)	calr3 GitHub	Oct 2026	Charlie Reams	Includes Lean formalization. Not independently verified.
Erdős Ternary Conjecture	Halts iff Erdős Problem 406 is false.	BB(15) BB(5,4)	BBi(19)	BB(15) machine 1RB1RO_0RC0RC_0RD1RJ_0LE1RC_0LF1LK_0LG1LE_0LH1LF_1RI0LL_0RB1LK_1RC0RA_0LI1LN_1RM---_0RI0RO_0LK1LK_1LM1RA (bbch) BB(5,4) and BBi(19) machine 1RB3RA2RA1RB_0LC2RB1RA3RB_0LD1LC2LE3LC_3RE2RE---1RE_0RB1LE2LE3LE (bbch)	bbchallenge, bbchallenge	Jul 2021	Tristan Stérin (@cosmo) 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." arxiv preprint. The BB(15) machine's behavior has been verified in Lean.
		BB(14)	BBi(27)	Machine code 1LB1RA_1LC1LB_0RD0RA_1LM0RE_1LF1RE_0LJ1LG_1RK0LH_1RI1LH_0LJ0RE_0RD1LJ_0LL1RK_1RN0LC_0LN---_0RK0LM (bbch)	Announced on Discord	Oct 2026	Tristan Stérin	Its behavior has been verified in Lean.
Erdős Ternary Conjecture variant	Halts iff the following conjecture (a variant of #406) is false: "For all n > 0, there is at least one 1 in the base-3 representation of 2^n - 1."	BB(4,4)	BBi(15)	Machine code 1RB2RA1RB3RA_0LC3RB2RB1RA_1RZ1LD2LC3LC_0RA1LD2LD3LD (bbch)	Announced on Discord	Oct 2026	roromachine14	Not independently verified.
Sloane Ternary Conjecture	Halts if and only if the following conjecture by N. J. A. Sloane is false: "For all n > 15, there is at least one 0 in the base-3 representation of 2^n."	BB(6,4)	BBi(21)	Machine code 2RB2RB1RA3RA_0LC1RB3RB2RA_0LE1LD2LC3LC_0RB1LD2LD3LD_1RD2RD3RD0LF_1RE2RZ------ (bbch)		Oct 2026	User:Loader3229	Not independently verified.
Ternary Conjecture variant	Halts if and only if a n such that 17*2^n has no digit 2 in base-3 exists.	BB(15)	BBi(29)	Machine code 1RB1LB_1LA1RN_0RE1RD_0RC1RC_0LH1RC_0LG1LH_---1LF_1LF0LL_0LJ1LK_0RD1LI_1LI0LL_1LM1LN_0LI0LI_0RO1LL_1LL0LO (bbch)		Oct 2026	Jacobzheng
Weak Collatz	Halts iff the weak Collatz conjecture is false.	BB(124) BB(43,4)	BBi(121)		bbchallenge, bbchallenge	Jul 2021	Tristan Stérin	The weak Collatz conjecture states that the iterated Collatz map (3x+1) has only one cycle on the positive integers (4 -> 2 -> 1 -> 4). This is a weakened version of the usual Collatz conjecture, since it does not exclude the possibility of integers that are not part of any cycle at all. Not independently verified.
		BB(14) BB(10,3)	BBi(26)	BB(14) machine code 1LM0RB_1LC1RB_0LM0LD_1RE1LD_0RF0RB_0LN0LG_1LH1LG_0RK0RI_1RJ1RI_0LN1RF_0RL1RK_0RZ1LC_0RA1LM_1LM1LN (bbch) BB(10,3) and BBi(26) machine code 2RG0RB---_1LC1RB2LC_0LI0LD2LD_1RE1LD1LF_2RC0RB---_0RJ2RG---_1RH1RG1RH_2LI1RC1RH_0RA1LI1LI_0LI1RJ1RZ (bbch)	calr3 on GitHub	Oct 2026	Charlie Reams	Includes Lean formalization. BB(14) verified by Shawn Ligocki.
Odd multiply perfect	Halts iff an odd multiply perfect greater than 1 exists.	BB(23,3)	BBi(63)	Machine code 1RO0RB2RF_1LL1RB2RC_0RC0LD2LI_0LD1LD2LE_1RA1LE0RA_0RF1LG2LM_0LG1LG2LH_0RA1LH0RA_1LI---2LJ_1LK1LJ1LK_1LL1LK---_2RA1LS---_1LM---2LN_0RO1LN2RR_2LW0RP2LJ_1LQ1RP2RP_1RO1LQ2LQ_2LG1RR2RR_0RT0LS0LS_0RT1RT2RU_0LV0RU0RU_0LV---2LW_2LB1LW--- (bbch)	Discord	Jul 2024	kg583	Not independently verified.
Odd perfect	Halts iff an odd perfect exists.	BB(37)	BBi(71)	Machine code	calr3 GitHub	Oct 2026	Charlie Reams	Includes Lean formalization. Not independently verified.
Brocard	Halts iff Brocard's problem n! + 1 = m2 has a solution with n > 7, i.e. beyond the known solutions n = 4, 5, 7.	BB(34)	BBi(66)	Machine code	GitHub (PR to google-deepmind/cryptids)	Nov 2026	Daniel Veljjanoski	Keeps n!/8 in unary and tests it for triangularity (n! + 1 = m2 forces m = 2k + 1, n!/8 = k(k+1)/2). Includes a Lean formalization (kernel-checked; PR pending). An earlier 61-state machine with a Lean proof is by Charlie Reams (calr3 GitHub, Nov 2026); a 43-state table without a machine-checked proof is in arXiv:2605.20215.
Kurepa	Halts if and only if Kurepa's conjecture is false.	BB(38)	BBi(65)	Machine code	calr3 GitHub	Oct 2026	Charlie Reams	Includes Lean formalization. Not independently verified.
Sierpiński	Halts iff 78,557 is the smallest Sierpiński number.	BB(60)	BBi(104)	Machine code	calr3 GitHub	Oct 2026	Charlie Reams	Includes Lean formalization. Not independently verified.
Riesel	Halts iff 509,203 is the smallest Riesel number.	BB(68)	BBi(112)	Machine code	loader3229 GitHub	Oct 2026	User:Loader3229 and DeepSeek	Includes Lean formalization. Not independently verified.
Fermat's Last Theorem	Does not halt.	BB(400)		Not provided.	Studies in Turing Machines (1965), pp. 81--82	1965	James Randels	From Randels' doctoral dissertation Studies in Turing Machines (1965). The machine was a cryptid until Wiles resolved Fermat's Last Theorem in 1994; it is now known that it cannot halt. The machine is not explicitly given, but there is a flowchart to construct the machine, and the state count is claimed to be less than 400.
		BB(90)	BBi(160)	Machine code	calr3 GitHub	Oct 2026	Charlie Reams	Includes Lean formalization. Not independently verified.
Bigfoot - compiled	Halts iff Bigfoot halts.	BB(7)	BBi(13)	Machine code 0RB1RB_1LC0RA_1RE1LF_1LF1RE_0RD1RD_1LG0LG_---1LB (bbch)	Bigfoot comment	June 2024	@Iijil1	Compilation of Bigfoot into 2 symbols, there was a previous compilation with 8 states.
Hydra - compiled	Halts iff Hydra halts.	BB(9)	BBi(15)	Machine code 0RB0LD_1LC0LI_1LD1LB_0LE0RG_1RF0RH_1RA---_0RD0LB_0RA---_0RF1RZ (bbch)	File:Hydra 9 states.txt	June 2024	@Iijil1	Compilation of Hydra into 2 symbols, all confirmed by Shawn Ligocki. @Iijil1 provided 24 TMs which all emulate the same behavior. Announced on Discord. Previous compilation had 10 states, by Daniel Yuan, also confirmed by Shawn Ligocki.

Cryptids for other BB-style functions

Beeping Busy Beaver

Cryptids were actually noticed in the Beeping Busy Beaver problem before they were in the classic Busy Beaver. See Mother of Giants describing a "family" of Turing machines which "probviously" quasihalt, but requires solving a Collatz-like problem in order to actually prove it. Mother of Giants are all TMs formed by filling in the missing transition in 1RB1LE_0LC0LB_0LD1LC_1RD1RA_---0LA with different values.

For a math problem encoded into a Π₂ statement but not a Π₁ statement, it can't encode into a TM halting problem, but it can encode into a TM quasihalting problem, so a BBB cryptid can be constructed from this problem.

Name	Behaviour	BBB domain	Machine	Source	Date	Discoverer	Note
Mother of Giants	Probviously quasihalting.	BBB(5)	Machine code 1RB1LE_0LC0LB_0LD1LC_1RD1RA_1RC0LA (bbch) and 3 others	Found "in the wild".	Apr 2022	Shawn Ligocki
Fermat Primes	Quasihalts iff there are only finitely many Fermat primes.	BBB(16)	Machine code (beep state: P) 1LO1LA_0LI0LC_0LD1LC_1RE1LD_0LF0RG_0RE1LF_0RH1RG_1RB1RH_---0LJ_1LK1LJ_1RA0LL_0LM0LL_0RN1RO_1RN1LA_1RO1RP_0LA0RB (bbch)	calr3 GitHub	Oct 2026	Charlie Reams	Not independently verified.
Twin prime conjecture	Quasihalts iff Twin Prime conjecture is false.	BBB(18)	Machine code (beep state: N) 1LB1RA_0LH0LC_0LD1LC_1RE1LD_0LF0RG_0RE1LF_0RA1RG_1RP1LI_1RL1LJ_1RP1LK_1RL1LK_0RM1RL_---0RN_0LB1RO_0LB1RO_1LQ1RP_1RR1LQ_---0RM (bbch)	calr3 GitHub	Oct 2026	Charlie Reams	Not independently verified.
Collatz	Quasihalts iff the Collatz conjecture is false.	BBB(17)	Machine code (beep state: O) 1RL0RB_1LC1RB_0LK0LD_1RE1LD_0RF0RB_0LG0LG_1LH1LG_0RA0RI_1RJ1RI_1RF1RF_0RA1LK_0LM0LM_0LN1LM_1RO1LN_0RA0RP_0RQ1RP_1RL1RQ (bbch)	Mira-Cult GitHub	Oct 2026	Mira Cult	Not independently verified.

BitChanger

Name	Domain	Machine	Date	Discoverer	Note
	Size 23 BitChanger programs	}}}<[}<}[}<<<]}}<[<<]}}]*	Apr 2025	mxdys	Similar random walk mechanism to Bigfoot. Probviously non-halting. Found "in the wild".

Boolfuck

Name	Domain	Machine	Date	Discoverer	Note
	BB_boolf(24)	*>*>*[>[*<<]*>*[<<]*>*>]	Oct 2026	sheep	Similar random walk mechanism to Bigfoot. Probviously non-halting. Translation of the smallest known BitChanger cryptid.

CounterScript

Name	Domain	Machine	Date	Discoverer	Note
	BBCS(23)	A++; B++; while B {while A {A--; C++; E++; while D {D--; E--;} while E {C++; D++; E--;}} C>>A; D>>B*3; B--;}	Jun 2026	sheep	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting.

Fractran

Name	Domain	Machine	Date	Discoverer	Note
Fenrir	BBf(22)	[1/15, 27/77, 49/3, 10/49, 33/2] and 2 others	Mar 2026	Jason Yuen (@-d) and Claude Opus 4.6	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting. Found "in the wild".
Frankenstein's Monster	BBf(23)	[1/12, 9/10, 14/3, 121/2, 5/7, 3/11]	Dec 2025	Shawn Ligocki	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting.
Antihydra-like Cryptid	BBf(23)	[9/10, 1/6, 1331/2, 14/3, 5/7, 3/11]	Dec 2025	maksandchael	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting.
11 Hydra-like Cryptids	BBf(23)	too many to display - see page	Aug 2026	Jason Yuen (@-d) and Claude Opus 4.6	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting. Found "in the wild".
Hydra - compiled	BBf(25)	[363/14, 125/2, 22/21, 1/3, 7/11, 14/5]	Dec 2025	maksandchael	Compilation of Hydra.
BMO 1 - compiled	BBf(36)	[153/55, 2/11, 26/35, 3/7, 11/17, 7/13, 25/6, 55/2, 14/3]	Nov 2025	maksandchael	Compilation of BMO 1.
	BBf(48)	[77/2, 2/99, 17/33, 13/11, 285/119, 17/19, 1375/51, 1/17, 3/5, 243/7, 10/13]	Nov 2025	maksandchael	Similar to Space Needle, probviously non-halting.

Lambda Calculus

Name	Domain	Machine	Date	Discoverer	Note
	BBλ(74)	$(\lambda 1111(\lambda 1)1(\lambda 2))(\lambda \lambda \lambda 1(322222))$	Apr 2025	50_ft_lock	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting.

Pebble Automaton

Name	Domain	Machine	Date	Discoverer	Note
	peBBle(12)	00_00_00_40_10_00_00_08_41_11_00_a1	Oct 2026	User:AlephSquirrel	Similar to BMO 1.
	peBBle(86)	https://discord.com/channels/960643023006490684/1535695107448381591/1554751839721750569	Sep 2026	sheep	Similar random walk mechanism to Hydra, Antihydra. Probviously non-halting.

Post Tag System

Name	Domain	Machine	Date	Discoverer	Note
	BB_PT(11)	11111_20_1	Jul 2026	sheep, Shawn Ligocki	This machine halts iff 5 eventually converges to 1 under the 5n+3 map.

Register machine

Name	Domain	Machine	Date	Discoverer	Note
	MBB(8)	0+B_1-FC_2-GD_0-EF_1+C_2+A_2-EH_1-B*	Oct 2026	Shawn Ligocki	Similar to Space Needle, probviously non-halting. An equivalent machine was analyzed. Found "in the wild".
Needle 1	MBB(8)	0+B_1+C_2-AD_1-EH_2+F_1-DG_0-EB_2-C*	Oct 2026	sheep	Similar to Space Needle, probviously non-halting. Found "in the wild".
Hydra - compiled	MBB(10)	0-BF_1+C_1+D_0-EH_1+A_2+G_2+I_2-I*_0+J_1-IA	Jun 2025	Shawn Ligocki	Compilation of Hydra.
5n+1	MBB(12,2)	0+B_0+C_0+D_0+E_1-IF_1+G_0-HE_0-FJ_0+A_1-KL_0+J_0-H*	Oct 2026	sheep	This machine halts iff 7 eventually converges to 1 under the 5n+1 map.
Erdős Ternary Conjecture	MBB(19)	4+B_4+C_0+D_0+E_2-CF_0-GI_2+H_1+F_1-JN_1-KN_1-LM_3+I_0+N_3-OQ_1+P_3-OI_0-RS_0-RE_4-E*	Sep 2026	mineralli	The machine halts if and only if the following conjecture by Erdős is false: "For all n > 8, there is at least one 2 in the base-3 representation of 2^n."
RH	MBB(130)	https://www.sciencedirect.com/science/article/pii/S0304397519304633	Feb 2020	Yuri Matiyasevich	The machine halts if and only if the Riemann hypothesis is false.

Wang Tiles

Name	Domain	Machine	Date	Discoverer	Note
ZFC	BBWT(11487)	https://github.com/jconorgrogan/k230-wang-tiles-lean	Oct 2026	jconorgrogan	These Wang tiles tile the whole integer plane if and only if Zermelo–Fraenkel set theory with the Axiom of Choice is consistent. Not independently verified.