바쁜 비버 게임

바쁜 비버 게임은 1962년 수학자 티보르 라도가 제안한 이론적인 컴퓨터 과학 문제입니다. 이 게임은 "비지 비버"라고 불리는 특수한 튜링 머신을 사용하는데, 이는 무한히 긴 종이 테이프에 가능한 한 많은 "1"을 쓰도록 설계된 프로그램입니다. 바쁜 비버 게임에서 양의 정수가 주어졌을 때, 상태(입력 알파벳과 상태 전환 함수 등)를 가진 모든 튜링 머신을 고려합니다. 이 게임의 목표는 빈 입력이 주어졌을 때 멈추기 전까지 가장 오랜 시간(또는 가장 많은 단계)이 걸리고, 가장 많은 1을 출력하는 튜링 머신을 찾는 것입니다. 이 출력에서 1의 개수는 튜링 머신의 상태 수인 n에 해당하는 양의 정수 BB(n)에 해당하는 바쁜 비버 함수의 값입니다.

2024년 9월, 20명 이상의 기여자로 구성된 팀은 47,176,870의 값을 갖는 다섯 번째 바쁜 비버 번호 BB(5)를 찾았다고 발표했습니다. 이 결과는 Tristan Stérin이 시작한 Busy Beaver Challenge 프로젝트의 일부로, BB(5)의 가치를 최종적으로 결정하는 것을 목표로 하는 온라인 협업입니다. 연구팀은 Coq 증명 어시스턴트라는 소프트웨어를 사용하여 연구 결과를 검증했습니다. Coq 증명 어시스턴트는 수학적 증명의 정확성을 보장하는 데 사용되는 공식 검증 도구입니다.