Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

Resumo Técnico: Um Estudo de Caso de Formalização do Problema do Grilo Utilizando a API Aristotle

Enunciado do Problema
Este artigo apresenta um estudo de caso de formalização do "Problema do Grilo", originalmente proposto como o Problema 6 da 50ª Olimpíada Internacional de Matemática (IMO 2009). O teorema afirma que, para qualquer conjunto de $n$ inteiros positivos distintos $\{a_1, \dots, a_n\}$ e um conjunto $M$ de $n-1$ inteiros positivos (onde a soma total $\sum a_i \notin M$), existe uma permutação $\sigma$ dos saltos tal que nenhuma soma parcial intermediária $S_k = \sum_{i=1}^k a_{\sigma(i)}$ atinja um elemento de $M$. O problema é notado por sua dificuldade histórica, tendo a pontuação média mais baixa entre todos os problemas da IMO de 2009, e exige raciocínio combinatório não trivial envolvendo permutações e conjuntos proibidos.

Metodologia
O estudo utiliza a API Aristotle, um sistema de prova automática de teoremas que combina busca guiada por modelos de linguagem, geração de lemas informais e formalização dentro do assistente de prova Lean 4 (utilizando Mathlib). Os autores forneceram um prompt específico à API Aristotle solicitando uma prova rigorosa e completa do Problema do Grilo, proibindo explicitamente citações do problema como um teorema conhecido e exigindo a construção de uma permutação válida.

O artefato resultante é um projeto Lean 4 contendo uma versão generalizada do teorema (permitindo $|M| < n$ em vez de estritamente $n-1$, e permitindo $0 \in M$). Os autores realizaram uma inspeção granular do código gerado para distinguir entre declarações totalmente verificadas por máquina e aquelas contendo marcadores de prova não resolvidos (sorry).

Principais Resultados e Componentes Verificados
O desenvolvimento Lean gerado não produziu uma prova completa do teorema principal. Em vez disso, resultou em um artefato híbrido consistindo em quatro lemas auxiliares totalmente verificados e um teorema principal não resolvido:

1. Componentes Locais Verificados:

   • PS last: Verificado que a soma parcial final é igual à soma total dos saltos.
   • PS swap: Verificado que uma transposição adjacente de saltos afeta apenas a soma parcial intermediária específica naquela posição, deixando todas as outras inalteradas.
   • PS swap eq: Verificada a forma algébrica da soma parcial alterada após uma troca ($S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$).
   • maximizer swap in M: Verificado um argumento de maximalidade local. Estabelece que, se uma permutação maximiza uma função de pontuação específica $G(\sigma)$, e uma soma parcial em uma posição trocável está em $M$, então o valor resultante da troca também deve estar em $M$.

2. Componente Global Não Resolvido:

   • O teorema principal, grasshopper, é encerrado diretamente por um único sorry.
   • O resumo da saída da API Aristotle identifica a etapa faltante como um argumento de contagem global. Enquanto os lemas locais estabelecem que trocas específicas forçam a pertinência a $M$, o sistema falhou em coordenar esses fatos para provar que eles geram pelo menos $n$ valores proibidos distintos, o que contradiria a suposição $|M| < n$. A fonte Lean não reduz o teorema principal a um lema de contagem separado e codificado; a lacuna permanece uma obrigação não provada.

Contribuições
O artigo faz duas contribuições primárias:

1. Um Artefato Reprodutível: Fornece uma tentativa de formalização em Lean 4 inspecionável e reprodutível de um problema difícil de combinatória olímpica utilizando a API Aristotle, incluindo o código-fonte completo e os registros de execução.
2. Uma Análise Precisa das Limitações da IA: Oferece uma dissecação detalhada do "status evidencial" de provas geradas por IA. O estudo demonstra que sistemas de IA podem verificar com sucesso etapas locais de raciocínio algébrico e baseado em trocas, enquanto falham em executar a contabilidade combinatória global necessária para encerrar o teorema principal.

Significância e Alegações
O artigo argumenta que a distinção entre "declarações verificadas" e "declarações encerradas por sorry" é crítica para a interpretação da prova de teoremas assistida por IA. A significância deste estudo de caso reside em sua demonstração de que a busca local por provas pode ter sucesso enquanto o raciocínio global permanece não resolvido.

Os autores enfatizam que uma compilação bem-sucedida de um arquivo Lean contendo sorry é evidência insuficiente de uma prova concluída. O artefato serve como um exemplo de cautela: embora ferramentas de IA possam gerar desenvolvimentos matemáticos substanciais e verificados (como os quatro lemas auxiliares), elas ainda podem deixar o motor lógico central da prova (a contradição global) não implementado. O artigo conclui que uma formalização assistida por IA confiável exige uma inspeção rigorosa das obrigações e dependências de prova, em vez de confiar na mera presença de código gerado.