No saguão de um hotel no centro de Londres, turistas se preparam para um dia de passeios sob uma onda de calor, enquanto acadêmicos se reúnem em uma sala sem janelas para discutir o papel da inteligência artificial (IA) na matemática contemporânea. O encontro, que envolve 25 pesquisadores de diversas áreas, tem como objetivo formalizar o Último Teorema de Fermat com o auxílio de modelos de IA de ponta.

O Último Teorema de Fermat, que intrigou matemáticos por séculos, foi provado em 1993 pelo matemático Andrew Wiles. A afirmação sustenta que não existem números inteiros a, b e c que satisfaçam a equação aⁿ + bⁿ = cⁿ, onde n é um número inteiro maior que 2. A simplicidade da declaração contrasta com a complexidade da prova.

Projeto de formalização em andamento

Kevin Buzzard, do Imperial College London, lidera um projeto de cinco anos que visa transformar as 100 páginas da prova de Wiles em um código de computador chamado Lean, permitindo que sua correção seja formalmente verificada e servindo como base para futuras pesquisas. Atualmente, mais de 2 milhões de linhas de matemática formalizada estão armazenadas em um repositório central chamado Mathlib.

Durante o workshop, grupos de pesquisadores se reúnem em torno de laptops, utilizando diferentes interfaces de um dos modelos de IA líderes da indústria. O ambiente é de concentração e colaboração, com os problemas sendo divididos e abordados por humanos que orientam a IA. O número de linhas de código no projeto dobrou em apenas um dia de trabalho, segundo Buzzard.

Desafios e perspectivas futuras

O projeto formalizará não apenas a prova final de Wiles, mas também considerará os fundamentos que sustentam essa prova, que se estendem por cerca de 2000 páginas de matemática anterior. Buzzard expressou confiança de que, ao final do projeto, conseguirá formalizar tudo o que se propôs, mas reconheceu que o progresso da IA e o custo de acesso a essas tecnologias influenciarão o resultado.

A pesquisadora Hang Lu Su, também do Imperial College London, utiliza ferramentas de IA como o ChatGPT para aprimorar suas habilidades em Lean. Ela acredita que a utilização de IA pode representar um vislumbre do futuro da matemática, mesmo que a maioria dos matemáticos ainda dependa de métodos tradicionais. Su destacou que a eficácia das ferramentas de IA pode mudar o modo como os matemáticos trabalham.

Entretanto, a implementação de código gerado por IA levanta questões sobre qualidade e eficiência. Buzzard alertou que o código pode ser verboso e ineficiente, o que pode dificultar sua integração no repositório Mathlib, que atualmente contém código escrito de forma precisa por matemáticos humanos.

Com o avanço da IA, surgem questões filosóficas sobre o papel dos matemáticos. Buzzard questionou o sentido do trabalho humano em matemática se máquinas puderem provar teoremas que os humanos não conseguem entender. Essa reflexão é especialmente pertinente em áreas da matemática que lidam com conceitos abstratos, levantando questões sobre a existência do conhecimento matemático na ausência da compreensão humana.