Virtual participation: Zoom details available here
Speaker: Dr Tristan Stérin, PRGM DEV, France
Title: "Formal verification of the 5th Busy Beaver value"
Abstract: Introduced in 1962 by Tibor Radó, the Busy Beaver value BB(n) is the maximum number of steps made by any n-state, 2-symbol deterministic halting Turing machine starting on blank tape. The function n ↦ BB(n) is noncomputable and, until very recently, only 4 of its values, BB(1) ... BB(4), were known -- the proof of "BB(4)=107" dating back to 1983.
In July 2024, an international team of computer scientists and mathematicians (bbchallenge.org) delivered a computerised proof of "BB(5) = 47,176,870", formalised using the Coq proof assistant software. In this talk, we'll introduce Busy Beaver values as well as the Coq proof assistant and give an overview of the techniques that were used to formally analyse the ~180 million 5-state Turing machines needed to prove the result, ending that way the 62-year-old quest of finding the 5th Busy Beaver value.
Biography: Tristan Stérin did his PhD in the fields of molecular computing and computer science under the supervision of Prof Damien Woods at the Hamilton Institute and department of computer science, Maynooth University, Ireland. During his PhD, he studied the Busy Beaver function which led him to launch the collaborative platform bbchallenge.org dedicated to proving "BB(5) = 47,176,870" in 2022. He also co-founded the R&D company prgm.dev which was recently awarded the Horizon Europe EIC Pathfinder grant DISCO on the topic of DNA data storage coordinated by Prof Damien Woods' group at Maynooth University.