As somebody not familiar with this field, is there any tangible benefit to this solution or is it purely academic?
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.
That's the incredible thing about these TMs - they are amazingly small but still can exhibit very complex behaviours - it's like microscopy for programs.
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 just want to know.
That's the reason why you were pointed to Hardy's Mathematician's Apology. He was talking about how his works would never have a practical use.
It turns out he was wrong, because Computers are mathematics made flesh. All these abstract notions suddenly had a practical use.
There is something fundamental about the limits of computing so there might well be something that can be made of the BB function but at the moment it's just pure maths.
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").
So the goals are hard to pin down exactly, but there are goals.
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.
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".