Uma coisa que sempre me atraiu na matemática é que o único domínio do conhecimento em que é possível dar respostas definitivas a, virtualmente, qualquer questão: quando um matemático prova (ou “desprova”) um teorema, esse debate se encerra e, simplesmente, avançamos para novas questões.

Em teoria, pelo menos. Na prática, conforme comentei aqui recentemente, em alguns casos a prova é tão complexa e sutil que fica difícil ter certeza se está correta ou não. E esse problema está se agravando, à medida que os trabalhos matemáticos se tornam mais longos e sofisticados. Felizmente, ferramentas computacionais avançadas estão entrando em campo para ajudar, e começamos a vislumbrar a possibilidade de que acabem fazendo esse trabalho por nós. Seus defensores vão mais longe, prognosticando que elas logo mudarão o modo como descobrimos novos resultados matemáticos.

A mais popular dessas ferramentas é o Lean, linguagem de programação e verificador de teoremas desenvolvido na Microsoft Research, em 2013, pela equipe do brasileiro Leonardo de Moura, doutor em ciência da computação pela PUC-Rio. Uma característica importante é que o Lean é interativo, ele pressupõe uma colaboração entre o matemático e o computador. Funciona mais ou menos assim.

O matemático formula o teorema que quer provar: é o seu Objetivo. Em seguida, escreve comandos curtos, como “simplifique”, “reescreva”, “aplique” etc. A cada vez, o Lean responde indicando quais são as suposições por trás do comando, e quais delas ainda falta provar, não deixando passar nenhuma lacuna de lógica. Assim, o Objetivo vai sendo decomposto em passos mais simples, até que todos tenham sido devidamente justificados. A essa altura, o Lean declara que o Objetivo foi alcançado: a veracidade da prova está formalmente comprovada.

Esse tipo de abordagem seria inviável se, a cada vez, todos os passos tivessem que ser justificados novamente a partir dos axiomas básicos da matemática. Em vez disso, o Lean vai coletando uma grande “biblioteca” (repositório) de teoremas que já foram verificados formalmente e, portanto, podem ser invocados diretamente na prova de novos teoremas. A MathlLib, como é chamada, já contém centenas de milhares de teoremas, formulados em mais de 2 milhões de linhas de código Lean.

Dito assim, pode até parecer fácil, mas não é: validar um teorema significativo em Lean é trabalhoso e demorado. Mas para alguns dos maiores especialistas da atualidade trata-se de uma oportunidade estratégica para a matemática, com enorme potencial de impacto sobre o futuro da disciplina. Entre os maiores defensores está ninguém menos do que Terence Tao, ganhador da medalha Fields em 2006, que até desenvolveu sua própria ferramenta de verificação de provas para assisti-lo em sua pesquisa.

Em janeiro de 2024, Tao e seu colega Alex Kontorovich lançaram o desafio de transcrever para Lean o Teorema dos Números Primos, um dos resultados mais importantes da teoria dos números. No mês passado, a empresa Math, Inc. (no Brasil seria “Matemática S.A.”) anunciou ter vencido esse desafio, com a ajuda de… inteligência artificial. Comentarei na semana que vem.

LINK PRESENTE: Gostou deste texto? Assinante pode liberar sete acessos gratuitos de qualquer link por dia. Basta clicar no F azul abaixo.