tsterin

use https://rocq-prover.org/ for that purpose

Opus 4.6 finds proofs of false in Rocq and Lean kernels.

45 minutes on 13 cores on a standard laptop :)

Thank you!

Yeah, one lesson is that if you relax your halting condition to entering a loop at some point you get much longer runtime, see machine Skelet#1 (https://bbchallenge.org/1LC1LE_---1LD_1RD0LD_1LA1RE_0LB0RC), enters a loop after 10^51 steps and the loop is 10^9 steps long.

Thank you!

Best compliment ever

In the paper we mention two other communities which seem to have similar structure and size:

- https://conwaylife.com/, on Conway's GoL and other cellular automata

- Googology, https://googology.fandom.com/wiki/Googology_Wiki and https://googology.miraheze.org/wiki/Main_Page, on big numbers

Number of 5-state TMs is 21^10 = 16,679,880,978,201; coming from (1 + writemovestate)^2*state; difference with your formula is that in our model, halting is encoded using undefined transition.

"essentially different" is not a statically-checked property. It is discovered by the enumeration algorithm (Tree Normal Form, see Section 3 of https://arxiv.org/pdf/2509.12337); in particular, for each machine, the algorithm needs to know it if will ever reach an undefined transition because if it does it will visit the children of that machine (i.e. all ways to set that reached undefined transition).

Knowing if an undefined transition will be ever reached is not computable, hence knowing the number of enumerated machines is not computable in general and is as hard as solving BB(5).

In Coq-BB5 machines are not run for 100M steps but directly thrown in the pipeline of deciders. Most halting machines are detected by Loops using low parameters (max 4,100 steps) and only 183 machines are simulated up to 47M steps to deduce halting.

In legacy bbchallenge's seed database, machines were run for exactly 47,176,870 steps, and we were left with about 80M nonhalting candidates. Discrepancy comes from Coq-BB5 not excluding 0RB and other minor factors.

Also, "There are 181 million ish essentially different Turing Machines with 5 states", it is important to note that we end up with this number only after the proof is completed, knowing this number is as hard as solving BB(5).

Repeatedly watching ChatGPT stream out words was giving me a headache, so I built ZenGPT: it hides responses until they’re fully generated.

https://chromewebstore.google.com/detail/zengpt/jcmppahlhehi... https://github.com/tcosmo/zengpt

I really like your point (I'm one of bbchallenge maintainers). I think that Discord is close to optimal for us in the short term, but bad for the reasons you and other have mentioned mid/long term.