BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formal verification of the 5th Busy Beaver value - Tristan Stérin
  (Maynooth University\, Ireland) and Maja Kądziołka
DTSTART:20250313T170000Z
DTEND:20250313T180000Z
UID:TALK226546@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION: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 machin
 e can perform from the all-0 tape before halting and S was historically in
 troduced as one of the simplest examples of a noncomputable function.\n\nU
 sing the Coq proof assistant\, we enumerate 181\,385\,789 5-state Turing m
 achines\, and for each\, decide whether it halts or not. Most of these mac
 hines are decided using new algorithms that simplify the halting problem b
 y building Finite State Automata to approximate the machine's set of reach
 able configurations. For 13 challenging Sporadic Machines\, we provide ind
 ividual Coq proofs of nonhalting.\n\nOur result marks the first determinat
 ion of a new Busy Beaver value in over 40 years\, leveraging Coq's computi
 ng capabilities and demonstrating the effectiveness of collaborative onlin
 e research.\n\n=== Hybrid talk ===\n\nJoin Zoom Meeting https://cam-ac-uk.
 zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1\n\nMeeting ID: 
 871 4336 5195\n\nPasscode: 541180
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR