O acervo do museu Getty, em Los Angeles, nos Estados Unidos, contém um retrato do século 17 de Euclides de Alexandria, matemático da Grécia antiga. A imagem o mostra desgrenhado, segurando páginas de "Os Elementos", seu tratado sobre geometria dividido em 13 livros, com as mãos sujas.
Por mais de 2.000 anos, os escritos do grego foram referência da argumentação e do raciocínio matemáticos.
Jeremy Avigad, professor de lógica na Universidade Carnegie Mellon, na Pensilvânia, diz que Euclides construiu sua argumentação de maneira reflexiva. "Provando as coisas de tal forma que cada passo sucessivo decorre claramente dos anteriores, usando as definições básicas e os teoremas prévios."
Profissionais do século 20, entretanto, já não estavam dispostos a fundamentar a matemática intuitivamente. Em vez disso, desenvolveram sistemas formais —representações simbólicas precisas, regras mecânicas. Com o tempo, essa formalização permitiu que a matemática fosse traduzida para código de computador.
Em 1976, o teorema de quatro cores, o qual afirma serem quatro cores o bastante para preencher um mapa de modo a não haver duas regiões adjacentes com a mesma cor, tornou-se a primeira proposição importante comprovada com ajuda de força computacional bruta.
Os matemáticos estão agora lidando com a força transformadora mais recente: a inteligência artificial. Christian Szegedy, cientista de computadores ex-Google, previu em 2019 que, nos próximos dez anos, sistema computadorizado igualaria ou superaria a capacidade de resolução de problemas dos melhores matemáticos humanos.
No entanto, Akshay Venkatesh, matemático do Instituto de Estudo Avançado da Universidade Princeton, em Nova Jérsei, e ganhador da Medalha Fields em 2018, não está interessado em usar IA no momento, mas quer muito falar sobre ela.
"Quero que meus alunos entendam que seu campo de trabalho vai mudar muito", declarou ele em entrevista no último ano. Recentemente, ele acrescentou em conversa por email não se opor ao uso ponderado e cuidadoso da tecnologia para apoiar a compreensão humana. Entretanto, acreditar fortemente ser essencial prestar atenção ao modo de utilização.
Em fevereiro deste ano, Venkatesh assistiu a um workshop no Instituto de Matemática Pura e Aplicada, no campus da UCLA (Universidade da Califórnia), sobre "provas assistidas por máquina". (Ele visitou o retrato de Euclides no dia final daquele dia).
O encontro atraiu um misto atípico de matemáticos e cientistas da computação. "Isso parece significativo", comentou Terence Tao, matemático da universidade, ganhador de uma Medalha Fields em 2006 e organizador principal do workshop.
Tao observou ter sido apenas nos últimos dois ou três anos que matemáticos começaram a se preocupar com as ameaças potenciais da IA, quer seja à estética matemática ou a eles próprios. O fato de membros eminentes da comunidade estarem agora falando do assunto e explorando o potencial da IA "meio que rompe o tabu", declara.
Um dos mais celebrados participantes do evento estava sentado na primeira fileira: uma caixa trapezoidal chamada "robô do levanta a mão". A máquina emitia um cochicho mecânico e levantava a mão sempre que um participante online tinha uma pergunta a fazer. "Ajuda se os robôs são bonitinhos e não parecem intimidadores", afirma Tao.
Hoje em dia não faltam gadgets para otimizar nossas vidas –nossa dieta, sono e exercício. "Gostamos de nos dotar de objetos a nos facilitar fazer as coisas corretamente", comenta Jordan Ellenberg, matemático da Universidade de Wisconsin-Madison, durante um intervalo no workshop.
Para ele, gadgets de IA podem fazer o mesmo para a matemática. "Está muito claro que a questão é o que as máquinas podem fazer por nós, e não o que as máquinas farão conosco."
Um gadget matemático é conhecido como assistente de prova ou comprovador interativo de teoremas (o "Automath" foi uma versão inicial na década de 1960). Eis como ele funciona: um matemático traduz uma prova em código. Depois, software verifica se o raciocínio está correto. As verificações se acumulam em uma biblioteca que outros podem consultar.
Esse tipo de formalização oferece um fundamento para a matemática hoje, diz Avigad, diretor do Centro Hoskinson de Matemática Formal (fundado pelo empreendedor de criptomoedas Charles Hoskinson). "Do mesmo modo como Euclides procurava codificar e fornecer uma base para a matemática de seu tempo."
Recentemente, o sistema de assistente de prova de fonte aberta Lean vem atraindo atenção. Desenvolvido na Microsoft por Leonardo de Moura, cientista da computação que agora está na Amazon, o Lean usa o raciocínio automatizado, alimentado pelo que é conhecida como a boa inteligência artificial à moda antiga, ou Gofai ("good old-fashioned artificial intelligence") –IA simbólica, inspirada na lógica.
Até agora a comunidade Lean já verificou um teorema interessante sobre virar uma esfera do avesso, além de um teorema fundamental para um esquema a unificar reinos matemáticos.
Mas um assistente de prova também tem desvantagens: frequentemente se queixa de não entender as definições, os axiomas ou os passos de raciocínio inseridos pelo matemático, razão pela qual já foi descrito como "reclamante da prova". Essas reclamações todas podem deixar as pesquisas trabalhosas.
Razão bruta –mas isso é matemática?
Outra ferramenta de raciocínio automatizado, usada por Marijn Heule, cientista da computação na Universidade Carnegie Mellon e estudioso da Amazon, é algo que ele chama coloquialmente de "raciocínio bruto" (o termo mais técnico é solucionador de satisfatibilidade, ou SAT).
Segundo ele, se você simplesmente declara, com codificação cuidadosamente elaborada, que tipo de "objeto exótico" visa encontrar, uma rede de supercomputadores vasculha um espaço de buscas e determina se esse objeto existe de fato.
Logo antes do workshop, Heule e um de seus alunos de doutorado, Bernardo Subercaseaux, finalizaram sua solução a um problema de longa data, com um arquivo de 50 terabytes. Mas esse arquivo mal era comparável a um resultado que Heule e seus colaboradores produziram em 2016.
"Prova de matemática de 200 terabytes é a maior de todos os tempos", anunciava manchete na revista Nature. O artigo questionava se resolver problemas com tais ferramentas poderia realmente ser visto como matemática. Para Heule, essa abordagem é necessária "para solucionar problemas que estão além do alcance humano".
Especialistas vêm reagindo a essas disrupções com graus diversos de preocupação.
Geordie Williamson, da Universidade de Sydney e colaborador da DeepMind incentiva seus colegas a se envolverem mais nessas discussões. "Considerando a probabilidade de todos sermos profundamente afetados nos próximos cinco anos, a aprendizagem profunda não tem estimulado tanta discussão quanto se poderia prever", diz.
Williamson considera a matemática um teste decisivo do que a aprendizagem de máquina é capaz ou não de fazer. O raciocínio, afirma ele, é essencial ao processo matemático e também principal dificuldade para mecanismos.
No início da colaboração de Williamson com a DeepMind, a equipe identificou uma rede neural simples que previu "uma quantidade na matemática com a qual eu me preocupava profundamente" e o fez "com precisão absurda".
O homem se esforçou muito para entender o porquê –isso daria o enunciado de um teorema--, mas não conseguiu. Tampouco seus colegas. Como Euclides, a rede neural de alguma maneira havia discernido uma verdade matemática intuitivamente, mas a razão lógica disso não era evidente.
No workshop de Los Angeles, um tema muito discutido foi como combinar o intuitivo e o lógico. Se a IA pudesse fazer as duas coisas ao mesmo tempo, as consequências seriam imprevisíveis.
Mas, observou Williamson, há pouca motivação para entender a caixa preta apresentada pela aprendizagem de máquina. "É a cultura do hacking na tecnologia: se uma coisa funciona na maior parte do tempo, então está ótimo". Isso, porém, deixa matemáticos insatisfeitos.
Tradução de Clara Allain
Comentários
Os comentários não representam a opinião do jornal; a responsabilidade é do autor da mensagem.