Determination of the fifth Busy Beaver value
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , , , , , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911536651436032 |
|---|---|
| author | The bbchallenge Collaboration Blanchard, Justin Briggs, Daniel Deka, Konrad Fenner, Nathan Forster, Yannick Georgiev, Georgi House, Matthew L. Hunter, Rachel Iijil Kądziołka, Maja Kropitz, Pavel Ligocki, Shawn mxdys Naściszewski, Mateusz savask Stérin, Tristan Xu, Chris Yuen, Jason Zimmermann, Théo |
| author_facet | The bbchallenge Collaboration Blanchard, Justin Briggs, Daniel Deka, Konrad Fenner, Nathan Forster, Yannick Georgiev, Georgi House, Matthew L. Hunter, Rachel Iijil Kądziołka, Maja Kropitz, Pavel Ligocki, Shawn mxdys Naściszewski, Mateusz savask Stérin, Tristan Xu, Chris Yuen, Jason Zimmermann, Théo |
| contents | 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. $S$ was historically introduced by Tibor Radó in 1962 as one of the simplest examples of an uncomputable function.
We prove that $S(5) = 47,176,870$ using the Coq proof assistant. The proof enumerates $181,385,789$ Turing machines with 5 states and, for each machine, decides whether it halts or not. 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, attesting to the effectiveness of massively collaborative online research (bbchallenge$.$org). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_12337 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Determination of the fifth Busy Beaver value The bbchallenge Collaboration Blanchard, Justin Briggs, Daniel Deka, Konrad Fenner, Nathan Forster, Yannick Georgiev, Georgi House, Matthew L. Hunter, Rachel Iijil Kądziołka, Maja Kropitz, Pavel Ligocki, Shawn mxdys Naściszewski, Mateusz savask Stérin, Tristan Xu, Chris Yuen, Jason Zimmermann, Théo Logic in Computer Science Formal Languages and Automata Theory Logic 03D10, 03B35 (Primary) 68Q05, 68Q45 (Secondary) F.1.1; F.4.1; I.2.3; D.2.4; F.4.3 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. $S$ was historically introduced by Tibor Radó in 1962 as one of the simplest examples of an uncomputable function. We prove that $S(5) = 47,176,870$ using the Coq proof assistant. The proof enumerates $181,385,789$ Turing machines with 5 states and, for each machine, decides whether it halts or not. 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, attesting to the effectiveness of massively collaborative online research (bbchallenge$.$org). |
| title | Determination of the fifth Busy Beaver value |
| topic | Logic in Computer Science Formal Languages and Automata Theory Logic 03D10, 03B35 (Primary) 68Q05, 68Q45 (Secondary) F.1.1; F.4.1; I.2.3; D.2.4; F.4.3 |
| url | https://arxiv.org/abs/2509.12337 |