Pesquisadores se reuniram em Londres esta semana para acelerar a formalização do Último Teorema de Fermat usando modelos avançados de IA. O workshop foca na conversão da prova de Andrew Wiles de 1993 em código Lean para verificação computacional. O progresso tem sido rápido, com as linhas de código dobrando após o primeiro dia.
Vinte e cinco matemáticos, cientistas da computação e especialistas em IA se encontraram em um hotel no centro de Londres para trabalhar no projeto liderado por Kevin Buzzard, do Imperial College London. O esforço de cinco anos, financiado em 2024, visa adicionar o teorema ao repositório Mathlib de matemática formalizada.
Antes do workshop, havia 20.000 linhas de código no projeto. Após o primeiro dia, o total atingiu 40.000. Buzzard observou que as capacidades de IA melhoraram drasticamente desde dezembro do ano passado, permitindo à equipe abordar mais aspectos da matemática subjacente do que o originalmente planejado.
Hang Lu Su, também do Imperial College London, descreveu o processo como uma industrialização do trabalho intelectual. Os participantes estão usando modelos, incluindo o Claude, para gerar e refinar o código, embora ainda existam preocupações sobre a verbosidade e a manutenibilidade a longo prazo das produções geradas por IA.
Buzzard expressou confiança de que os objetivos originais serão cumpridos até o fim do projeto. O quanto a equipe avançará na pirâmide completa de teoremas de suporte dependerá de desenvolvimentos futuros em IA.