Determination of the Fifth Busy Beaver Value

> Structure of the proof. The proof of our main result, Theorem 1.1, is given in Section 6. The structure of the proof is as follows: machines are enumerated arborescently in Tree Normal Form (TNF) [9] – which drastically reduces the search space’s size: from 16,679,880,978,201 5-state machines to “only” 181,385,789; see Section 3. Each enumerated machine is fed through a pipeline of proof techniques, mostly consisting of deciders, which are algorithms trying to decide whether the machine halts or not. Because of the uncomputability of the halting problem, there is no universal decider and all the craft resides in creating deciders able to decide large families of machines in reasonable time. Almost all of our deciders are instances of an abstract interpretation framework that we call Closed Tape Language (CTL), which consists in approximating the set of configurations visited by a Turing machine with a more convenient superset, one that contains no halting configurations and is closed under Turing machine transitions (see Section 4.2). The S(5) pipeline is given in Table 3 – see Table 4 for S(2,4). All the deciders in this work were crafted by The bbchallenge Collaboration; see Section 4. In the case of 5-state machines, 13 Sporadic Machines were not solved by deciders and required individual proofs of nonhalting, see Section 5.

So, they figured out how to massively reduce the search space, wrote some generic deciders that were able to prove whether large amounts of the remaining search spaces would halt or not, and then had to manually solve the remaining 13 machines that the generic deciders couldn't reason about.

Second, you have to consider what's feasible in finite time. You can enumerate machines and also enumerate proofs, but any concrete strategy has limits. In the case of BB(5), the authors did not use naive brute force. They exhaustively enumerated the 5-state machines (after symmetry reductions), applied a collection of certified deciders to prove halting/non-halting behavior for almost all of them, and then provided manual proofs (also formalized) for some holdout machines.

For example:

https://teorth.github.io/equational_theories/

https://teorth.github.io/pfr/

- 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

https://bbchallenge.org/13650583

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).

Is there some reason why Rocq is the proof assistant of choice and not one of the others?

also.... https://www.youtube.com/watch?v=c3sOuEv0E2I

Is this suspected or proven? I would love to read the proof if it exists.

Working on it did make people cleverer at analyzing the behavior of software, but it's not obvious that those skills or associated techniques will directly transfer to analyzing the behavior of much more complex software that does practical stuff. The programs that were being analyzed here are extraordinarily small by typical software developer standards.

To be more specific, it seems conceivable to me that some of these methods could inspire deductive techniques that can be used in some way in proof assistants or optimizing compilers, in order to help ensure correctness of more complicated programs, but again that application isn't obvious or guaranteed. The people working on this collaboration would definitely have described themselves as doing theoretical computer science rather than applied computer science.

This particular proof is doubly-academic in the sense that the value was already known, this is just a way to make it easier to independently verify the result.

It's a part of a broader movement to provide machine proofs for other stuff (e.g., Fermat's last theorem), which may be beneficial in some ways (e.g., identifying issues, making parts of proofs more "reusable").

G. H. Hardy's autobiography was titled "A Mathematician's Apology" because he, somewhat jokingly, wanted to apologize for a life of pure math... totally academic and completely useless.

Then a few years after he passed away, his math was key for The Manhattan Project to build the first successful nuclear bomb. His math lead to the device that changed the world and affected every aspect of human life for a century.

It's only "useless" until someone finds a "use".

P.S. The book documents his time with Ramanujan. If you liked the film "The Man Who Knew Infinity", you should read Apology

I don't like to call this "purely academic" because that sounds dusty and smells moth-chewed and utterly boring. It's purely spiritual, purely heart-warming, purely brain-flexing.

It's like asking a mountain climber whether reaching K2 has practical benefits or if it's "academic".

One benefit is that it is related to foundations of mathematics. If you can find busy beaver number 745, you can prove or disprove Maths. If you can find busy beaver 6, you can prove few collatz like conjecture which is an open problem.

Most core research doesn't help directly, but through indirect means. e.g. This would have led to finding the areas of improvements in Lean due to its complexity. I know for fact that Lean community learns a lot from projects like Mathlib and this. And Lean is used in all sort of scenarios like making AWS better to improving safety of flights.

The underlying result has not changed, but the presentation of the details is now complete.

But taken more generally, not for this specific instance, your question is actually a Millenium Prize problem worth a million dollars.