University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Formal verification of the 5th Busy Beaver value

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Formal verification of the 5th Busy Beaver value

Download to your calendar using vCal

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.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180

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

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Brain Repair Centre, Forvie Site, Addenbrookes MRL meeting rooms 1 & 2, Level 4 Institute of Metabolic Sciences, Addenbrooke’s Treatment Centre (ATC) interesting

Other talks

Dwarf Galaxies in the Local Universe What Can a Spectrum Learn? AI Perspectives on the Kohn Laplacian of Sphere Quotients Title to be confirmed Formal Dinner at Selwyn College CSAR lecture: 46&: Development of a probiotic that supports the natural removal of forever chemicals from the body A Data-Centric Approach to AI Adaptation and Alignment
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity