Formal verification of the 5th Busy Beaver value

Add to your list(s) Download to your calendar using vCal

• Tristan Stérin (Maynooth University, Ireland) and Maja Kądziołka
• Thursday 13 March 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

We prove that S(5) = 47,176,870. The Busy Beaver value S(n) gives the maximum number of steps a halting n-state 2-symbol Turing machine can perform from the all-0 tape before halting and S was historically introduced as one of the simplest examples of a noncomputable function.

Using the Coq proof assistant, we enumerate 181,385,789 5-state Turing machines, and for each, decide whether it halts or not. Most of these machines are decided using new algorithms that simplify the halting problem by building Finite State Automata to approximate the machine’s set of reachable configurations. For 13 challenging Sporadic Machines, we provide individual Coq proofs of nonhalting.

Our result marks the first determination of a new Busy Beaver value in over 40 years, leveraging Coq’s computing capabilities and demonstrating the effectiveness of collaborative online research.

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.