Em um recanto misterioso da ciência da computação, um enigma de quarenta anos – o problema da lontra ocupada – foi recentemente resolvido por um grupo de amadores. Essa conquista não apenas causou sensação no meio acadêmico, mas também recebeu o reconhecimento do renomado matemático Terence Tao, que compartilhou a notícia nas redes sociais, destacando a importância dos assistentes de prova na pesquisa matemática.
O cientista da computação Scott Aaronson também elogiou muito a descoberta, considerando-a o avanço mais significativo na pesquisa da função da lontra ocupada desde 1983. Essa conquista marca uma compreensão mais profunda dos limites da teoria da computação e demonstra o potencial das provas assistidas por software na resolução de problemas matemáticos complexos.
O problema da lontra ocupada surgiu há mais de 40 anos em Dortmund, na Alemanha, quando cientistas da computação tentaram encontrar a 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 computacional abstrato, proposto por Alan Turing em 1936, que realiza cálculos lendo e escrevendo 0s e 1s em uma fita infinitamente longa.
Em 1974, após a determinação do quarto número da lontra ocupada, a busca pelo quinto se tornou um problema em aberto. Agora, uma comunidade online composta por mais de 20 colaboradores de todo o mundo, usando o software assistente de prova chamado Coq, conseguiu verificar o valor do quinto número da lontra ocupada, BB(5), como sendo 47.176.870.
Essa conquista não apenas agitou a comunidade, mas também causou admiração no cientista da computação Damien Woods, que comparou esse avanço à velocidade de Bolt. Embora a solução do problema possa não ter aplicações diretas em outras áreas da ciência da computação, para os participantes, a luta contra a impossibilidade matemática em si já é a maior recompensa.
O cerne do problema da lontra ocupada reside na compreensão do comportamento das máquinas de Turing, especialmente seu desempenho no problema da parada. O comportamento de uma máquina de Turing é definido por um conjunto de regras, que podem ser imaginadas como uma tabela. Cada regra especifica a operação a ser executada quando a cabeça de leitura/escrita encontra um 0 ou um 1 em um determinado estado.
Embora as máquinas de Turing possam entrar em loops infinitos, determinar se elas irão parar é um famoso problema não resolvido. O matemático Tibor Radó não ficou satisfeito com essa conclusão e, portanto, inventou o "jogo da lontra ocupada", explorando a natureza do problema da parada agrupando as máquinas de Turing de acordo com o número de regras que possuem.
Pesquisadores iniciais, como Allen Brady, exploraram esse problema simulando o comportamento das máquinas de Turing por meio da programação. Seu trabalho e as descobertas de outros pesquisadores lançaram as bases para exploradores posteriores.
Até 2022, o pós-graduando Tristan Stérin lançou o "Desafio da Lontra Ocupada", um projeto de colaboração online com o objetivo de finalmente determinar BB(5). Por meio de métodos inovadores e com a ajuda do assistente de prova Coq, a equipe finalmente encontrou a quinta lontra ocupada.
Essa conquista não é apenas um desafio à impossibilidade matemática, mas também uma exploração dos limites da ciência da computação. Com a confirmação de BB(5), os pesquisadores estão redigindo um artigo acadêmico, que será uma versão legível para humanos que complementa a prova Coq. Ao mesmo tempo, eles estão pensando se a exploração de BB(6) será o próximo objetivo.
Referências: https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/