With fifth busy beaver, researchers approach computation's limits
Researchers led by graduate student Tristan Stérin determined BB(5) as 47,176,870 using Coq software. Busy beavers, introduced by Tibor Radó, explore Turing machines' behavior. Allen Brady's program efficiently analyzes and classifies machines, advancing computational understanding.
Read original article
Researchers have made a significant breakthrough in the field of computer science by determining the value of BB(5), a number that quantifies the complexity of simple computer programs known as busy beavers. The team, led by graduate student Tristan Stérin, used the Coq proof assistant software to verify the value as 47,176,870. This achievement marks a milestone in understanding the limits of computation and the halting problem, a fundamental challenge in computer science. The hunt for busy beavers involves analyzing Turing machines, theoretical devices that simulate computation. The concept of busy beavers was introduced by mathematician Tibor Radó, who devised the "Busy Beaver game" to explore the runtime behavior of Turing machines with different numbers of rules. The quest for busy beavers requires sophisticated computational tools due to the vast number of possible machine configurations. Allen Brady, a mathematics graduate student, made significant contributions to the field by developing a computer program to analyze and classify Turing machines efficiently. Brady's work exemplifies the intersection of mathematics, computation, and theoretical computer science in unraveling the mysteries of busy beavers and the halting problem.
Related
Rosser's Theorem via Turing Machines (2011)
The post delves into Rosser's Theorem, a potent extension of Gödel's Incompleteness Theorems, showcasing self-reference in formal systems. It elucidates Rosser's stronger disproof concept and its impact on system consistency. Additionally, it links Rosser's Theorem to the halting problem's unsolvability, underlining computational insights and Gödel's lasting influence on computability theory.
A modern 8 bit design, built using 1950s thermionic valves
A modern 8-bit Valve.Computer, using 1950s valves, plays games like PONG and runs a 32-bit Fibonacci sequence. Built over 18 months, it integrates valves into a functional system, managed informally with colored pens. Despite challenges, the project was successful, with plans for art installation.
The good, the bad, and the weird (2018)
Trail of Bits delves into "weird machines" in software exploitation, complex code snippets evading security measures. Techniques like Hoare triples and dynamic_casts aid in identifying and preventing exploitation, crucial in evolving security landscapes.
Chomsky–Schützenberger Enumeration Theorem
The Chomsky-Schützenberger enumeration theorem connects formal language theory and abstract algebra, focusing on word counts in unambiguous context-free grammars. It has applications in combinatorics and highlights ambiguity in certain languages.
Getting the World Record in Hatetris (2022)
David and Felipe set a world record in HATETRIS, a tough Tetris version. They used Rust, MCTS, and AlphaZero concepts to enhance gameplay, achieving a score of 66 points in 2021.
21 commentsAnd for leisure-class beavers, some big related threads from earlier this year:
https://news.ycombinator.com/item?id=40453221
One such variant is a functional busy beaver defined in terms of the lambda calculus [1]. Since it measures program size in bits rather than states, it allows many more values to be determined (37 so far versus only 6 for TMs), and the gap between the largest known value and values beyond Graham's Number is a mere 13 program bits. A closely related variant [2] can be directly expressed in terms of Kolmogorov complexity, which Mikhail Andreev argues [3] is crucial for applications in Information Theory.
For a modern version of the paper with some additional notes, see https://data.jigsaw.nl/Rado_1962_OnNonComputableFunctions_Re...
Note that there have been computer-assisted proofs before (four-color theorem, Kepler's conjecture), but those were not done in a formally verified setting until later.
By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.
I find it interesting that the description of Brady's program to optimize search for BB(4) by cutting out search subtrees whose differences don't matter is fairly close to a description of what I did to make my program fast.
Edit: number of TM for n states: (4n + 1)^(2n). Found this (for smaller n), which is the kind of analysis I was curious about: https://github.com/LukasKalbertodt/beaver
When talking about the limits of human knowledge, I often think about the theorems that are provable, but so complex that no human being could understand them. Probably the most complex proof we have is the classification of finite simple groups, which is thousands upon thousands of pages, and there is probably very few or no people on Earth that fully understand all of it.
As the article suggests, BB(6) could be undecidable. But it could also have a proof millions of pages long, beyond the reach of humanity.
> You need to find a mathematical reason why it can’t halt, and there’s no systematic method for finding such reasons—that was the great discovery of Gödel and Turing nearly a century ago.
That's only true for sufficiently large N, large enough to encode the halting paradox. (How large is that N? It's larger than 5!) Smaller N can and do fall to systematic methods.
> (x) = (5x+18)/3 if x = 0 (mod 3),
The second = should be \equivalent. This is a rare case where that actually matters, because is being used in both non-modular integer operations (divide by 3) and modular operations (where division by 3 is not defined).
BB(1) = 1
BB(2) = 4
BB(3) = 6
BB(4) = 13
They just proved that BB(5) = 47,176,870.
It is known that BB(6) must be at least 10^10^...^10 (a tower of exponents fifteen levels high).
https://en.wikipedia.org/wiki/Busy_beaver#Known_values_for_%...
my team has also proved this via our production codebase
> To distill the essence of the halting problem into a simpler form, Radó imagined sorting Turing machines into groups based on how many rules they had — one group for all one-rule Turing machines, another for all two-rule machines, and so on. Sure, that leaves infinitely many such groups, since a Turing machine can have any number of rules. But the number of distinct machines in every group is finite, since there are only so many possible combinations of rules.
> With two rules, there are already over 6,000 distinct Turing machines to consider; that number swells to millions with three rules, and to billions with four.
I'm pretty sure the standard terminology is "states", not "rules". This deviation made it harder to understand.
Each state produces 2 transition rules, depending on the symbol at the tape head.
Related
Rosser's Theorem via Turing Machines (2011)
The post delves into Rosser's Theorem, a potent extension of Gödel's Incompleteness Theorems, showcasing self-reference in formal systems. It elucidates Rosser's stronger disproof concept and its impact on system consistency. Additionally, it links Rosser's Theorem to the halting problem's unsolvability, underlining computational insights and Gödel's lasting influence on computability theory.
A modern 8 bit design, built using 1950s thermionic valves
A modern 8-bit Valve.Computer, using 1950s valves, plays games like PONG and runs a 32-bit Fibonacci sequence. Built over 18 months, it integrates valves into a functional system, managed informally with colored pens. Despite challenges, the project was successful, with plans for art installation.
The good, the bad, and the weird (2018)
Trail of Bits delves into "weird machines" in software exploitation, complex code snippets evading security measures. Techniques like Hoare triples and dynamic_casts aid in identifying and preventing exploitation, crucial in evolving security landscapes.
Chomsky–Schützenberger Enumeration Theorem
The Chomsky-Schützenberger enumeration theorem connects formal language theory and abstract algebra, focusing on word counts in unambiguous context-free grammars. It has applications in combinatorics and highlights ambiguity in certain languages.
Getting the World Record in Hatetris (2022)
David and Felipe set a world record in HATETRIS, a tough Tetris version. They used Rust, MCTS, and AlphaZero concepts to enhance gameplay, achieving a score of 66 points in 2021.