Non formal proof with a program March 2023: www.sligocki.com/2023/03/13/skelet-1-infinite.html Awesome article that describes the proof procedure.
The proof uses Turing machine acceleration to show that Skelet machine #1 is a Translated cycler Turing machine with humongous cycle paramters:
The Busy beaver scale allows us to gauge the difficulty of proving certain (yet unproven!) mathematical conjectures!
To to this, people have reduced certain mathematical problems to deciding the halting problem of a specific Turing machine.
A good example is perhaps the Goldbach's conjecture. We just make a Turing machine that successively checks for each even number of it is a sum of two primes by naively looping down and trying every possible pair. Let the machine halt if the check fails. So this machine halts iff the Goldbach's conjecture is false! See also Conjecture reduction to a halting problem.
Therefore, if we were able to compute , we would be able to prove those conjectures automatically, by letting the machine run up to , and if it hadn't halted by then, we would know that it would never halt.
Of course, in practice, is generally uncomputable, so we will never know it. And furthermore, even if it were computable, it would take a lot longer than the age of the universe to compute any of it, so it would be useless.
However, philosophically speaking at least, the number of states of the equivalent Turing machine gives us a philosophical idea of the complexity of the problem.
The busy beaver scale is likely mostly useless, since we are able to prove that many non-trivial Turing machines do halt, often by reducing problems to simpler known cases. But still, it is cute.
But maybe, just maybe, reduction to Turing machine form could be useful. E.g. The Busy Beaver Challenge and other attempts to solve BB(5) have come up with large number of automated (usually parametrized up to a certain threshold) Turing machine decider programs that automatically determine if certain (often large numbers of) Turing machines run forever.
So it it not impossible that after some reduction to a standard Turing machine form, some conjecture just gets automatically brute-forced by one of the deciders, this is a path to
If you can reduce a mathematical problem to the Halting problem of a specific turing machine, as in the case of a few machines of the Busy beaver scale, then using Turing machine deciders could serve as a method of automated theorem proving.
That feels like it could be an elegant proof method, as you reduce your problem to one of the most well studied representations that exists: a Turing machine.
However it also appears that certain problems cannot be reduced to a halting problem... OMG life sucks (or is awesome?): Section "Turing machine that halts if and only if Collatz conjecture is false".
bbchallenge.org/story#what-is-known-about-bb lists some (all?) cool examples,
- BB(15): Erdős' conjecture on powers of 2, which has some relation to Collatz conjecture
- BB(27): Goldbach's conjecture
- BB(744): Riemann hypothesis
- BB(748): independent from the Zermelo-Fraenkel axioms
- BB(7910): independent from the ZFC
wiki.bbchallenge.org/wiki/Cryptids contains a larger list. In June 2024 it was discovered that BB(6) is hard.
Turing machine that halts if and only if the Goldbach conjecture is false by 
Ciro Santilli 37 Updated 2025-07-16
Ciro Santilli 37 Updated 2025-07-16 Turing machine that halts if and only if Collatz conjecture is false by Ciro Santilli 37 Updated 2025-07-16
Ciro Santilli 37 Updated 2025-07-16mathoverflow.net/questions/309044/is-there-a-known-turing-machine-which-halts-if-and-only-if-the-collatz-conjectur suggests one does not exist. Amazing.
Intuitively we see that the situation is fundamentally different from the Turing machine that halts if and only if the Goldbach conjecture is false because for Collatz the counter example must go off into infinity, while in Goldbach conjecture we can finitely check any failures.
Amazing.
Complexity: NP-intermediate as of 2020:
- expected not to be NP-complete because it would imply NP != Co-NP: cstheory.stackexchange.com/questions/167/what-are-the-consequences-of-factoring-being-np-complete#comment104849_169
- expected not to be in P because "could we be that dumb that we haven't found a solution after having tried for that long?
In this case, the problem becomes equivalent to reversing modular exponentiation.
This computational problem forms the basis for Diffie-Hellman key exchange, because modular exponentiation can be efficiently computed, but no known way exists to efficiently compute the reverse function.
Like Binary search tree, but each node can have multiple objects and more than two children.
Pinned article: Introduction to the OurBigBook Project
Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
Intro to OurBigBook
. Source. We have two killer features:
- topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculusArticles of different users are sorted by upvote within each article page. This feature is a bit like:
- a Wikipedia where each user can have their own version of each article
- a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
Figure 1. Screenshot of the "Derivative" topic page. View it live at: ourbigbook.com/go/topic/derivativeVideo 2. OurBigBook Web topics demo. Source. - local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
Figure 3. Visual Studio Code extension installation.
Figure 4. Visual Studio Code extension tree navigation.
Figure 5. Web editor. You can also edit articles on the Web editor without installing anything locally.Video 3. Edit locally and publish demo. Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.Video 4. OurBigBook Visual Studio Code extension editing and navigation demo. Source. 
- Infinitely deep tables of contents:
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact