💻 computer science

Determination of the fifth Busy Beaver value

Este artigo relata a determinação formalmente verificada, utilizando o assistente de prova Coq, do quinto valor Busy Beaver como $S(5) = 47.176.870$ , marcando a primeira descoberta de um novo valor dessa função em mais de 40 anos através de uma pesquisa colaborativa online.

Autores originais: The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Sha

Publicado 2026-03-24

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Naściszewski, savask, Tristan Stérin, Chris Xu, Jason Yuen, Théo Zimmermann

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você tem um robô muito simples, chamado Máquina de Turing. Ele tem uma fita infinita de papel (com zeros e uns), uma cabeça que lê e escreve, e um "cérebro" com um número limitado de estados (como "pensando", "escrevendo", "parando").

O jogo do Busy Beaver (ou "Preguiçoso Ocupado") é uma competição entre esses robôs. A regra é simples:

Você dá a eles uma fita totalmente em branco (todos zeros).
Eles começam a trabalhar.
O objetivo é: quem consegue dar o maior número de passos antes de parar?

Quanto mais passos o robô dá, mais "ocupado" ele foi. O problema é que, para robôs com muitos estados, a matemática diz que é impossível criar uma regra geral para prever se eles vão parar ou ficar rodando para sempre. É um mistério matemático.

O Grande Desafio: O Robô de 5 Estados

Durante décadas, os matemáticos conseguiram resolver o mistério para robôs pequenos:

Robô de 1 estado: Para rápido.
Robô de 2 estados: Para depois de 6 passos.
Robô de 3 estados: Para depois de 21 passos.
Robô de 4 estados: Para depois de 107 passos.

Mas o Robô de 5 estados era um monstro. Em 1989, alguém descobriu um robô que trabalhava por 47.176.870 passos antes de parar. A pergunta que ficou pendente por 35 anos foi: "Existe algum outro robô de 5 estados que trabalhe ainda mais do que esse?"

Se a resposta fosse "sim", o recorde seria quebrado. Se fosse "não", então 47 milhões seria o número máximo possível.

A Solução: Uma Colaboração Gigante e um "Advogado Robô"

Este artigo conta a história de como um grupo enorme de pessoas (cientistas, programadores, estudantes e entusiastas de todo o mundo, reunidos no site bbchallenge.org) resolveu esse quebra-cabeça.

Eles não tentaram simular cada robô um por um (seria impossível, pois existem trilhões de combinações). Em vez disso, eles usaram uma estratégia inteligente:

O Pente Fino (TNF): Eles criaram um método para organizar os robôs em uma "árvore genealógica", eliminando duplicatas e robôs que nunca chegariam a lugar nenhum. Isso reduziu o número de robôs a analisar de 16 trilhões para "apenas" 181 milhões.
Os Detetives (Deciders): Eles criaram vários "detetives" (algoritmos). Cada detetive tinha uma especialidade:
- Um detectava robôs que entravam em um loop infinito (como um hamster correndo numa roda).
- Outro olhava para padrões repetitivos na fita (como se o robô estivesse cantando a mesma música).
- Outros usavam lógica complexa para provar que certos robôs nunca parariam.
O Advogado Robô (Coq): Aqui está a mágica. Eles usaram um software chamado Coq, que é como um "advogado matemático" super rigoroso. O Coq não confia em ninguém; ele exige provas formais.
- Os humanos escreveram os códigos dos detetives.
- O Coq verificou cada linha de código para garantir que os detetives não estavam mentindo.
- O Coq então "correu" a prova, verificando cada um dos 181 milhões de robôs.

O Veredito Final

Depois de meses de trabalho e milhões de horas de processamento de computador, o Coq chegou à conclusão:

Não existe robô de 5 estados que trabalhe mais do que 47.176.870 passos.

O robô descoberto em 1989 é, de fato, o vencedor. O valor S(5) = 47.176.870 foi provado matematicamente.

Por que isso é importante?

Primeira vez na história: É a primeira vez que um novo valor do "Busy Beaver" foi descoberto em mais de 40 anos.
Confiança total: Antes, as provas eram feitas por humanos com programas que podiam ter erros. Agora, temos uma prova verificada por um computador que não comete erros de lógica. É a prova mais confiável que já tivemos.
O que vem a seguir? O artigo mostra que, para robôs de 6 estados, o problema se torna impossível de resolver com a matemática atual. Existem "monstros" (chamados de Cryptids) que podem estar ligados a problemas famosos como a Conjectura de Goldbach ou a Hipótese de Riemann. Resolver o robô de 6 estados pode exigir que a humanidade resolva esses mistérios antigos primeiro.

Resumo em uma frase

Um time global de voluntários, usando um "advogado de computador" super rigoroso, provou que o robô mais preguiçoso e ocupado de 5 estados parou exatamente após 47.176.870 passos, encerrando um mistério de 35 anos e abrindo a porta para os desafios matemáticos mais difíceis do futuro.

Título: Determinação do Quinto Valor do Busy Beaver

Autores: A Colaboração bbchallenge (Justin Blanchard, Daniel Briggs, Konrad Deka, et al.)
Ferramenta Principal: Assistente de Prova Coq (Coq-BB5)

1. O Problema

O problema do Busy Beaver (Preguiçoso), introduzido por Tibor Radó em 1962, busca determinar o valor da função $S(n)$ , que representa o número máximo de passos que uma Máquina de Turing com $n$ estados e 2 símbolos pode executar a partir de uma fita vazia (todos zeros) antes de parar.

A função $S(n)$ é incomputável (não existe um algoritmo geral para calculá-la para todo $n$ ).
Historicamente, apenas os primeiros quatro valores foram provados: $S(1)=1$ , $S(2)=6$ , $S(3)=21$ e $S(4)=107$ .
O valor de $S(5)$ permaneceu um problema em aberto por mais de 40 anos. Em 1989, Heiner Marxen e Jürgen Buntrock encontraram uma máquina de 5 estados que executa 47.176.870 passos, estabelecendo um limite inferior. A conjectura era que esta seria a máquina vencedora, mas a prova de que nenhuma outra máquina de 5 estados pudesse superar esse número (ou que todas as outras parariam antes) nunca foi formalizada.

2. Metodologia

A solução foi alcançada através de uma colaboração massiva online (bbchallenge.org) e formalizada matematicamente usando o assistente de prova Coq. A metodologia envolveu três pilares principais:

A. Enumeração em Forma Normal de Árvore (TNF)

Para lidar com o espaço de busca gigantesco (aproximadamente $1,67 \times 10^{13}$ máquinas sintáticas), os autores utilizaram a Tree Normal Form (TNF).

A TNF elimina máquinas com transições inalcançáveis e permutações redundantes de estados/símbolos.
Isso reduziu o espaço de busca de 16,7 trilhões para 181.385.789 máquinas únicas a serem analisadas.
A enumeração e a execução da verificação foram implementadas diretamente dentro do Coq, garantindo que nenhuma máquina fosse esquecida.

B. Pipelines de Decisores (Deciders)

Como o problema da parada é indecidível, não existe um único algoritmo para determinar se uma máquina para. A equipe desenvolveu um "pipeline" de múltiplos algoritmos (decisores) que tentam provar se uma máquina para ou não para:

Loops (Ciclos): Detecta máquinas que entram em ciclos infinitos (Cyclers) ou ciclos transladados no espaço (Translated Cyclers). Este método resolveu ~95% das máquinas que não param.
NGramCPS (Conjunto de Posição Fechada n-gram): Uma técnica de interpretação abstrata que modela o comportamento local da fita usando n-gramas. Resolveu ~99,89% das máquinas restantes que não param.
RepWL (Lista de Palavras Repetidas): Utiliza expressões regulares para simular blocos de símbolos na fita, detectando padrões de repetição.
FAR e WFAR (Redução por Autômatos Finitos): Técnicas baseadas em autômatos finitos (determinísticos e ponderados) para provar a não-parada de máquinas mais complexas ("irregulares").
Simulação Direta: Para máquinas que param, simula-se até o limite de 47.176.870 passos.

C. Máquinas Esporádicas (Sporadic Machines)

13 máquinas específicas não foram resolvidas pelos decisores automatizados. Elas exigiram provas individuais de não-parada construídas manualmente e formalizadas no Coq. Estas máquinas exibem comportamentos complexos, como:

Skelet #1: Um ciclo transladado com um pré-período de $5,41 \times 10^{51}$ passos.
Skelet #10: Um contador duplo em base Fibonacci.
Skelet #17: Um mecanismo complexo de codificação Gray e listas de inteiros.

3. Principais Contribuições e Resultados

Resultados Principais

Prova de $S(5) = 47.176.870$ : O artigo prova formalmente que a máquina descoberta em 1989 é, de fato, a vencedora. Nenhuma outra máquina de 5 estados executa mais passos.
Prova de $\Sigma(5) = 4.098$ : O número máximo de 1s na fita para uma máquina de 5 estados que para.
Prova de $S(2, 4) = 3.932.964$ : Determinação do valor para máquinas de 2 estados e 4 símbolos.
Confirmação de $S(4) = 107$ : Revalidação formal do resultado anterior.

Estatísticas do Processo

Máquinas Analisadas: 181.385.789 máquinas de 5 estados.
Tempo de Compilação: A prova Coq compila em cerca de 45 minutos em 13 núcleos (usando otimizações native_compute).
Código: O projeto Coq-BB5 possui cerca de 27.000 linhas de código Coq e 638 lemas (mais 10.000 linhas de provas importadas).
Validação: A prova depende apenas de um axioma padrão do Coq (functional_extensionality_dep), que é amplamente aceito.

4. Significado e Impacto

Primeira Validação Formal: Este é o primeiro valor de Busy Beaver a ser formalmente verificado por um assistente de prova. Isso elimina qualquer dúvida sobre erros de implementação em softwares personalizados ou erros humanos na análise de "holdouts" (máquinas não resolvidas).
Colaboração em Massa: O projeto demonstra a eficácia da pesquisa colaborativa online ("bbchallenge.org"), onde centenas de contribuidores (muitos sem afiliação acadêmica) desenvolveram algoritmos, discutiram casos e validaram resultados em um ambiente de "construção pública".
Fronteira da Computabilidade: O trabalho esclarece a fronteira entre o que é provável e o que é indecidível.
- Para $n=5$ , o problema é difícil, mas solucionável com técnicas computacionais e formais.
- Para $n \ge 6$ , o artigo identifica "Cryptids" (como a máquina Antihydra), cujos problemas de parada podem ser equivalentes a conjecturas matemáticas profundas (como a Conjectura de Collatz) ou até independentes de sistemas axiomáticos como a Aritmética de Peano (PA) ou ZFC.
Avanço em Verificação Formal: O uso do Coq para enumerar e executar algoritmos de decisão sobre máquinas de Turing representa um marco em "provas por reflexão" (proofs by reflection), onde o assistente de prova executa o próprio algoritmo de verificação.

Conclusão

O artigo encerra um capítulo de 40 anos na teoria da computação, provando que $S(5) = 47.176.870$ . Mais do que apenas um número, o trabalho estabelece um novo padrão de rigor para problemas de complexidade computacional, combinando colaboração distribuída, inteligência artificial (na busca de padrões) e verificação formal rigorosa. Ele também fornece um mapa detalhado da "zoologia" das máquinas de Turing de pequeno porte, categorizando comportamentos como contadores, fractais e helicoides, e aponta para os desafios extremos que aguardam na classe de 6 estados.