Researchers Formally Verify Fifth Busy Beaver Value S(5) = 47,176,870 Using Coq Proof Assistant
By
marvinborner
Toasted golden, schmeared with insight. Top of the rack.
Summary
A collaborative research team has successfully determined the fifth Busy Beaver value S(5) = 47,176,870 using the Coq proof assistant, marking the first new Busy Beaver value discovery in over 40 years and the first to be formally verified. The proof involved enumerating 181,385,789 Turing machines with 5 states and determining whether each halts, representing a major breakthrough in theoretical computer science and computability theory.
Key quotes
· 4 pulledWe prove that $S(5) = 47,176,870$ using the Coq proof assistant.
The Busy Beaver value $S(n)$ is the maximum number of steps that an $n$-state 2-symbol Turing machine can perform from the all-zero tape before halting.
Our result marks the first determination of a new Busy Beaver value in over 40 years and the first Busy Beaver value ever to be formally verified.
The proof enumerates $181,385,789$ Turing machines with 5 states and, for each machine, decides whether it halts or not.
You might also wanna read
The Busy Beaver Problem: Recent BB(5) Breakthrough and the Antihydra Challenge
The article explores the busy beaver problem in theoretical computer science, focusing on the recent breakthrough in determining BB(5) as 47
benbrubaker.com·7mo ago
Feedback Distillation: A New Training Method for Improving LLM Reasoning in Theorem Proving
This paper introduces Feedback Distillation, a novel training method for reasoning models that improves upon standard GRPO (Group Relative P
arxiv.org·4h ago
Why Stochastic Rounding Prevents Error Accumulation in Low-Precision Arithmetic
This article explains the critical difference between round-to-nearest and stochastic rounding in low-precision floating-point arithmetic (B
convergentthinking.sh·2d ago
Bayesian Gaussian Process Modeling for Uncertain Spatial Coordinates Using PyMC
This article discusses the use of Bayesian spatial probability models, specifically Gaussian processes (GPs), for handling data with uncerta
christopherkrapu.com·7d ago
Cleve Moler, MATLAB Creator and MathWorks Cofounder, Dies at 86
Cleve Moler, cofounder of MathWorks and creator of the MATLAB programming language, passed away on May 20, 2026, at age 86. Moler was a math
mathworks.com·10d ago
ERA: A tree-search-based scientific coding tool for computational discovery
ERA (Empirical Research Assistance) is a versatile tool for scientific coding that can search scientific literature, write code, explore sol
research.google·12d ago