Viewing profile — 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…

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, ht…

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

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) a…

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…

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 mention…