O problema do castor ocupado, um problema da ciência da computação que já dura quarenta anos, foi finalmente resolvido por um grupo de amadores! Este desenvolvimento inovador não só chocou a comunidade académica, mas também foi reconhecido pelo famoso matemático Terence Tao, e foi aclamado como o desenvolvimento mais importante neste campo desde 1983. Usando o assistente de prova Coq, eles verificaram com sucesso que o valor do quinto número do castor ocupado BB(5) é 47.176.870, demonstrando o grande potencial da prova assistida por software na resolução de problemas matemáticos complexos e também nos fornecendo insights sobre o comportamento da máquina de Turing. e interromper problemas com uma nova perspectiva.
Em uma área misteriosa da ciência da computação, um problema de quarenta anos chamado problema do castor ocupado foi recentemente resolvido com sucesso por um grupo de amadores. Essa conquista não só causou sensação no mundo acadêmico, mas também foi reconhecida pelo famoso matemático Terence Tao, que encaminhou a notícia nas redes sociais e enfatizou a importância dos assistentes de prova na pesquisa matemática.
O cientista da computação Scott Aaronson também elogiou esta descoberta, acreditando ser o desenvolvimento mais importante na pesquisa da função do castor desde 1983. Esta conquista marca uma compreensão profunda dos limites da teoria computacional e demonstra o potencial das provas assistidas por software na resolução de problemas matemáticos complexos.
O problema do castor ocupado originou-se há mais de 40 anos em Dortmund, na Alemanha, quando cientistas da computação tentaram encontrar uma máquina de Turing específica que pudesse escrever o maior número de 1 antes de parar. Uma máquina de Turing é um modelo de computação abstrato proposto por Alan Turing em 1936 que realiza cálculos em uma fita magnética infinitamente longa lendo e escrevendo 0s e 1s.
Depois que o número do quarto castor ocupado foi determinado em 1974, encontrar o quinto castor tornou-se uma questão em aberto. Agora, uma comunidade online de mais de 20 colaboradores de todo o mundo, usando um software assistente de prova chamado Coq, verificou com sucesso que o quinto número BB(5) do Busy Beaver tem um valor de 47.176.870.
Essa conquista não apenas empolgou a comunidade, mas também despertou o espanto do cientista da computação Damien Woods, que comparou o progresso à velocidade de Usain Bolt. Embora a solução para este problema possa não ser diretamente aplicável a outras áreas da ciência da computação, para os participantes, esta luta contra a impossibilidade matemática é a maior recompensa por si só.
O núcleo do problema do castor ocupado reside na compreensão do comportamento das máquinas de Turing, especificamente no seu desempenho em problemas de parada. O comportamento de uma máquina de Turing é definido por um conjunto de regras, que pode ser imaginado como uma tabela. Cada regra especifica uma ação que deve ser executada quando o cabeçote de leitura/gravação encontra um 0 ou 1 em um estado específico.
Embora as máquinas de Turing possam ficar presas em loops infinitos, determinar se elas param de funcionar é um problema notoriamente não resolvido. O matemático Tibor Radó não ficou satisfeito com esta conclusão e, portanto, inventou o "jogo do castor ocupado" para explorar a natureza do problema da parada agrupando as máquinas de Turing de acordo com o número de regras que possuíam.
Os primeiros pesquisadores, como Allen Brady, exploraram esse problema escrevendo programas para simular o comportamento de máquinas de Turing. Seu trabalho e as descobertas de outros pesquisadores lançaram as bases para exploradores posteriores.
Até 2022, o estudante de pós-graduação Tristan Stérin lançou o Busy Beaver Challenge, um projeto colaborativo online que visa finalizar o BB(5). Através de métodos inovadores e com a ajuda do assistente de prova Coq, a equipe finalmente conseguiu encontrar o quinto castor ocupado.
Esta conquista não é apenas um desafio à impossibilidade da matemática, mas também uma exploração dos limites da ciência da computação. Com a confirmação do BB(5), os pesquisadores estão elaborando um artigo acadêmico que será uma versão legível por humanos que complementa a prova Coq. Ao mesmo tempo, também estão a pensar se a exploração do BB(6) se tornará o próximo alvo.
Referência: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
A solução para o problema do castor ocupado não é apenas um grande avanço no campo da matemática, mas também fornece novas direções e ideias para futuras pesquisas em teoria da computação. Essa conquista incentiva mais pessoas a participarem da pesquisa em matemática e ciências da computação e a explorarem áreas desconhecidas juntas.