Computação e Teoremas da Matemática

Talvez por influência de um doutorando em matemática, que está trabalhando com provador de teoremas computacionais, achei interessante o texto abaixo:

Há uma infecção de software na matemática pura. Alguns dos intelectuais peso-pesados do campo, renomados por sua autoconfiança, estão começando a se voltar para software para ajudá-los a entender e verificar provas.

Kevin Buzzard, um teórico dos números e professor de matemática pura do Imperial College London, acredita que agora é a hora de criar uma área na matemática dedicada a provas computadorizadas. As maiores provas para teoremas se tornaram tão complexas que praticamente nenhum humano na Terra pode entender todos os seus detalhes, quanto mais verificá-las. Ele teme que muitas provas consideradas verdade estão erradas. É preciso ajuda de fora.

O que é uma prova? Uma prova é uma demonstração da verdade num teorema. Ao provar tais teoremas, e ao aprender novas técnicas para esse processo, as pessoas evoluem o conhecimento de matemática, que depois é filtrado em outros campos.

Para criar uma prova, comece com algumas definições, ou axiomas. Por exemplo, defina um conjunto de números como números inteiros, todos os números de negativo infinito para positivo infinito. Escreva esse conjunto como: … , -2, -1, 0, 1, 2, … Em seguida, exponha um teorema, por exemplo, que não há um número inteiro maior. A prova então consiste no raciocínio lógico que mostra que o teorema é verdadeiro ou falso - neste caso, verdadeiro. Os passos lógicos na prova dependem de outras verdades anteriores, que já foram aceitas e provadas. Por exemplo, que o número 1 é menor que 2.


Novas provas de matemáticos profissionais tendem a depender de toda uma gama de resultados anteriores que já foram publicados e entendidos. Mas Buzzard diz que há muitos casos onde essas provas anteriores usadas para construir novas provas são claramente não entendidas. Por exemplo, há artigos notáveis que citam abertamente trabalhos que não foram publicados. Isso preocupa Buzzard.

“Agora estou preocupado pensando que toda a matemática publicada está errada, porque os matemáticos não estão conferindo os detalhes, e já vi eles errarem antes”, contou Buzzard ao Motherboard enquanto participava da décima conferência Interactive Theorem Proving em Portland, Oregon, onde ele deu uma palestra.

“Acho que há uma chance acima de zero de que alguns dos nossos castelos tenham sido construídos na areia”, Buzzard escreveu numa apresentação de slides. “Mas acho que é pequena.”


Novas teorias matemáticas deveriam ser provadas do zero. Cada passo precisa ser conferido, ou pelo menos esse é o raciocínio. Por outro lado, há especialistas sêniores e mais antigos da comunidade de matemática que fornecem um guia de testemunho confiável para o que é verdade e o que não é. Se um desses matemáticos mais velhos cita um artigo e o usa em seu trabalho, então o artigo provavelmente não precisaria ser conferido, segundo esse pensamento.

Buzzard aponta que essa matemática moderna se tornou dependente demais dos antigos porque os resultados se tornaram muito complexos. Uma nova prova pode citar outros 20 artigos, e só um desses 20 pode envolver mil páginas de raciocínio denso. Se um matemático respeitado cita o artigo de mil páginas, ou constrói sua teoria sobre ele, então muitos outros matemáticos podem supor que esse artigo de mil páginas (e a nova prova) é verdadeiro e não vão se dar ao trabalho de conferi-lo. Mas matemática deveria ser universalmente provável, não dependente de um punhado de especialistas.

Essa dependência excessiva dos matemáticos antigos leva a uma fragilidade na compreensão da verdade. Uma prova do Último Teorema de Fermat, proposto em 1637 e que já foi considerado pelo Guinness o “problema matemático mais difícil” do mundo, foi publicada nos anos 1990. Buzzard propõe que ninguém realmente a entende completamente, ou sabe se a prova é mesmo verdade.

“Acredito que nenhum humano, vivo ou morto, conhece todos os detalhes da prova do Último Teorema de Fermat. Mas a comunidade aceita a prova mesmo assim”, Buzzard escreveu em sua apresentação. Porque “os matemáticos antigos decretaram que a prova está certa”.

Alguns anos atrás, Buzzard assistiu palestras dos matemáticos sêniores Thomas Hales e Vladimir Voevodsky, que o apresentaram a um software de verificação de provas que estava se tornando muito bom. Com esse software, as provas podiam ser verificadas sistematicamente por um computador, as tirando das mãos dos matemáticos antigos e democratizando o status da verdade.

Quando Buzzard começou a usar o software de verificação de provas chamado Lean, ele ficou viciado. Não só o software permitia que ele verificasse provas além de qualquer dúvida, ele também o ajudava a pensar sobre matemática de um jeito claro e inconfundível.

“Percebi que computadores só aceitam inputs numa forma muito precisa, que é o meu jeito favorito de pensar em matemática”, disse Buzzard. “Me apaixonei pelo software, porque foi como encontrar uma alma gêmea. Descobri algo que pensava em matemática do mesmo jeito que eu.”

Para verificar sua prova, um usuário do Lean tem que formalizar a prova, ou a converter da linguagem humana para símbolos da linguagem de programação do Lean. O usuário também precisa formalizar quaisquer definições e provas subsidiárias de que o novo trabalho depende. E mesmo que esse processo de conversão seja trabalhoso, o Lean parece capaz de lidar com qualquer matemática que Buzzard joga nele, o que o distingue de outros programas assistentes de provas.

O Lean tem atraído interesse de uma comunidade crescente de matemáticos, particularmente na área de ensino. Jeremy Avigad é um professor da Universidade Carnegie Mellon especializado em teoria da prova. Tanto Avigad como Buzzard começaram a usar o Lean em aulas universitárias introdutórias de prova. O software verifica a veracidade de cada linha de uma prova e dá um feedback, o que é útil para os estudantes.

Apesar de Avigad estar empolgado com a comunidade que se interessou pelo Lean, ele alerta que a tecnologia ainda precisa de melhorias. Assistentes de provas exigem muito tempo para usar. “O campo existe há algumas décadas e as coisas estão melhorando, mas ainda não chegamos lá”, afirmou.


Se esses desafios puderem ser superados, Buzzard acredita que o software pode ter efeitos ainda mais amplos além de provas. Por exemplo, o problema da busca. Grandes quantidades de novos trabalhos são publicados todo ano, em grande velocidade, tornando a busca através dessas provas extremamente importante.

Hales e Buzzard apontaram que se todos os resumos de artigos fossem colocados no Lean, então qualquer matemático poderia consultar a base de dados desses resumos por um tema matemático preciso do Lean, e encontrar tudo que é sabido sobre ele. Até certo ponto, os cérebros inescrutáveis dos matemáticos antigos poderiam ser virados do avesso.

Cientistas da computação poderiam usar uma base de dados para treinar inteligências artificiais. Como os resultados dessa base de dados seriam definidos pela linguagem precisa do Lean, seria muito mais fácil para um programa aprender do que de resultados comparados escritos em inglês idiossincrático.

No final das contas, cientistas da computação poderia criar um provador geral de teoremas automatizado, um sistema de software que pode criar suas próprias provas e fazer sua própria matemática. Provadores automatizados dependem da mesma tecnologia do Lean para determinar se uma prova é verdadeira. O aumento da adoção do Lean pode se tornar um passo formativo importante para uma matemática automatizada no geral.

O Helix Center de Manhattan vai fazer uma mesa redonda de discussão sobre automação da matemática em 5 de outubro, transmitida ao vivo no YouTube e no site deles. Michael Harris, professor de matemática da Universidade de Columbia e colega de Buzzard, vai participar do fórum.

Harris teme que cientistas da computação e empresas de tecnologia que querem automatizar a matemática não compartilhem as mesmas motivações que os matemáticos. Cientistas da computação, por exemplo, querem usar a tecnologia por trás do Lean para se certificar de que programas não tenham bugs. Empresas querem lucro. Matemáticos como Buzzard só querem fazer matemática.

“Uma coisa que posso prever é que se pessoas realmente inteligentes como Thomas Hales e Buzzard continuarem a pensar nessa linha, então algo interessante vai sair disso; pode não ser uma IA, mas podem ser novos ramos da matemática ou novas maneiras de pensar”, imagina Harris.