🤖 AI

Case study: proving sqrt(2) irrational with LPTP and an LLM

Este artigo apresenta um estudo de caso demonstrando como um LLM, guiado por definições básicas de programação lógica e verificado pelo provador de teoremas LPTP, pode gerar com sucesso uma prova formal completa e legível por humanos da irracionalidade da raiz quadrada de 2.

Autores originais: Fred Mesnard, Étienne Payet, Wim Vanhoof

Publicado 2026-07-24

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Fred Mesnard, Étienne Payet, Wim Vanhoof

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um detetive tentando resolver um mistério que intriga os humanos há mais de dois mil anos: a raiz quadrada de 2 é um número "racional"? No mundo da matemática, um número racional é como uma fração perfeita, uma fatia limpa de uma torta (como 3/4 ou 5/2). Um número irracional é um decimal bagunçado e infinito que nunca pode ser escrito como uma fração simples. A raiz quadrada de 2 é o comprimento da diagonal de um quadrado com lados de comprimento 1, e matemáticos antigos provaram que ela é bagunçada — não pode ser uma fração.

Agora, imagine que você tem duas ferramentas muito diferentes para ajudar a resolver isso. A primeira é um árbitro superestrito e robótico chamado LPTP. Ele fala uma linguagem muito precisa e lógica (baseada em Prolog) e só aceitará uma prova se cada passo for matematicamente perfeito. Se você cometer até mesmo um erro minúsculo, ele baterá o martelo e dirá: "Não, inválido." A segunda ferramenta é um Modelo de Linguagem de Grande Escala (LLM), que é como um aluno superinteligente e criativo que leu quase tudo o que já foi escrito. Este aluno é ótimo em adivinhar o próximo passo de uma história ou de um problema matemático, mas às vezes ele "alucina", inventando fatos que parecem bons, mas que são errados.

A grande questão para os cientistas hoje é: podemos unir esses dois? Podemos deixar o aluno criativo fazer o trabalho pesado de escrever a prova, enquanto o árbitro estrito verifica cada frase para garantir que o aluno não esteja mentindo? Este artigo explora exatamente essa parceria, usando o antigo mistério da raiz quadrada de 2 como o caso de teste.

A Grande Parceria de Verificação de Provas

Neste artigo, os autores propõem-se a ver se conseguem usar uma IA moderna (especificamente, um modelo chamado Claude) para ajudar a provar que a raiz quadrada de 2 é irracional, mas com um detalhe: a prova tinha de ser escrita num formato muito específico e rigoroso que o árbitro robótico (LPTP) pudesse compreender e verificar. Eles não queriam apenas que a IA dissesse "é verdade"; eles queriam que a IA escrevesse a própria lógica passo a passo, que seria então graduada pelo árbitro.

A história começa com uma ideia simples. Para provar que a raiz quadrada de 2 é irracional, normalmente assume-se o contrário: que ela é uma fração composta por dois números inteiros, $p$ e $q$ , que não partilham quaisquer fatores comuns (eles são "primos entre si" ou coprimos). Se fizer a matemática, acaba por encontrar uma contradição onde ambos os números devem ser pares, o que significa que eles partilham um fator (2). Isso quebra a regra de que eram coprimos, provando que a suposição original estava errada.

Os autores tentaram fazer com que a IA escrevesse esta prova na linguagem estrita do LPTP. No início, a IA era como um aluno que conhece a história, mas não consegue escrever a redação no formato exigido. Ela tentava saltar passos ou fazer saltos lógicos que o árbitro não aceitaria.

É aqui que aconteceu o trabalho de equipe. Os autores estabeleceram um ciclo de feedback:

A IA tenta escrever um passo da prova.
O árbitro (LPTP) verifica-o.
Se o árbitro encontrar um erro, ele aponta a linha exata onde a lógica falhou.
Os autores mostram esse erro à IA.
A IA tenta novamente, corrigindo o erro específico.

Este processo era como um jogo de "quente ou frio". O árbitro não dizia apenas "errado"; ele dizia: "Cometeste um erro no passo 4", permitindo que a IA corrigisse o seu curso.

Os Resultados: Uma Vitória Parcial

O experimento foi um sucesso, mas com algumas ressalvas. A IA foi capaz de provar muitos dos componentes menores e mais fáceis do puzzle por conta própria. Por exemplo, provou com sucesso que "se um número é par, o seu quadrado é par" ou que "2 vezes um número é par". Os autores chamam a estas "lemmas" (pequenas provas auxiliares). A IA acertou nestas, chegando por vezes a criar novas ideias auxiliares que os humanos não tinham pensado.

No entanto, para a parte mais difícil da prova — a lógica específica que mostra por que razão a raiz quadrada de 2 não pode ser uma fração — a IA ficou bloqueada. Não conseguiu encontrar o caminho certo sozinha. Assim, os autores humanos tiveram de intervir e dar à IA uma "dica" ou até escrever a estrutura principal da prova eles próprios, pedindo à IA que preenchesse as lacunas menores.

No final, produziram uma prova formal completa de que a raiz quadrada de 2 é irracional. Esta prova foi parcialmente escrita pela IA e totalmente verificada pelo árbitro robótico. O árbitro atribuiu-lhe uma nota de aprovação, confirmando que a lógica era sólida.

O Que Isto Significa

O artigo não afirma que a IA possa agora resolver todos os problemas matemáticos sozinha. De facto, os autores mostram explicitamente que a IA não consegue fazê-lo sozinha; sem a orientação humana e a verificação estrita do árbitro, a IA provavelmente teria produzido uma prova falsa ou quebrada.

Em vez disso, o artigo sugere uma nova forma de trabalhar: IA como escritora de rascunhos, humanos como editores e ferramentas formais como verificadores de factos. A IA é rápida e criativa, gerando ideias e preenchendo detalhes, enquanto a ferramenta formal (LPTP) atua como um olho implacável que deteta alucinações e erros.

Os autores também testaram outras ferramentas matemáticas automatizadas (chamadas ATPs) para ver se conseguiam fazer o trabalho mais rapidamente. Estas ferramentas eram rápidas e gratuitas, mas produziam provas que eram difíceis de ler para os humanos e que não podiam ser facilmente adicionadas à biblioteca de matemática verificada. A abordagem da IA, embora mais lenta e que requer ajuda humana, produziu provas que eram legíveis e que podiam ser armazenadas com segurança para uso futuro.

Em suma, este artigo mostra que não precisamos de escolher entre a intuição humana e a precisão da máquina. Ao deixar a IA fazer o trabalho pesado de redação e as ferramentas estritas fazerem a graduação, podemos construir um sistema onde a IA nos ajuda a provar verdades matemáticas complexas, desde que mantenhamos um humano no comando para guiar o navio e um árbitro estrito para verificar o mapa. A raiz quadrada de 2 continua a ser irracional, mas agora temos uma nova forma colaborativa de a provar.

Resumo Técnico: Estudo de Caso Provando a Irracionalidade de $\sqrt{2}$ com LPTP e um LLM

Enunciado do Problema
O artigo aborda o desafio de provar formalmente que a raiz quadrada de 2 é irracional no contexto de Programação Lógica (LP). Especificamente, os autores visam provar que não existem dois números naturais coprimos $p$ e $q$ tais que $p^2 = 2q^2$ . Embora este seja um resultado matemático clássico, os mecanismos de programação lógica baseados em resolução padrão (como o Prolog) não podem fornecer uma resposta negativa à consulta correspondente porque o espaço de busca sobre números naturais é infinito. Os autores buscam preencher essa lacuna utilizando o sistema LPTP (Logic Program Theorem Prover) para gerar uma prova formal e avaliar até que ponto um Grande Modelo de Linguagem (LLM) pode auxiliar na construção desta prova.

Metodologia
Os autores empregam uma abordagem híbrida combinando o sistema de verificação formal LPTP com um LLM (especificamente o Claude Opus 4.5 da Anthropic).

Estrutura Formal (LPTP):
- O LPTP é utilizado para verificar propriedades de programas lógicos baseados em lógica de primeira ordem e na completude de Clark.
- O sistema distingue entre sucesso, falha e terminação de predicados usando operadores específicos ( $S$ , $F$ , $T$ ) e suporta esquemas de indução para predicados recursivos.
- A linguagem de prova é baseada em dedução natural, garantindo a legibilidade humana.
- Os autores definem o problema usando predicados de Prolog puro para números naturais (aritmética de Peano), adição, multiplicação e MDC.
Estratégia de Integração com LLM:
- Aprendizado em Contexto (In-Context Learning): O LLM recebe o manual do usuário do LPTP (PDF) e duas bibliotecas básicas (números de Peano e listas) contendo código Prolog e provas existentes.
- Ciclo de Feedback Iterativo: Os autores submetem lemas ao LLM em sintaxe LPTP (ou linguagem natural). O LLM gera uma tentativa de prova, que é imediatamente alimentada no verificador de provas LPTP.
- Correção de Erros: Se o verificador LPTP rejeitar a prova, ele reporta o primeiro passo de derivação incorreto. Este erro específico é retroalimentado ao LLM para refinar a prova.
- Supervisão Humana: Um desenvolvedor humano gerencia a ordem dos lemas, decide quando abandonar loops improdutivos e fornece dicas de alto nível ou a estrutura da prova para etapas difíceis.
Ferramentas Auxiliares:
- Os autores também utilizaram provadores de teoremas de Lógica de Primeira Ordem (ATP) prontos para uso, como Vampire e E, traduzindo axiomas LPTP para sintaxe FOF. Estes foram utilizados para verificar lemas de forma independente, embora suas provas baseadas em resolução não pudessem ser diretamente integradas ao framework de dedução natural do LPTP.

Principais Contribuições e Resultados

Construção de Prova: A equipe construiu com sucesso uma prova formal completa e verificada por máquina da irracionalidade de $\sqrt{2}$ no LPTP. A prova foi parcialmente gerada pelo LLM e totalmente validada pelo verificador LPTP.
Geração de Lemas:
- O LLM provou com sucesso vários lemas auxiliares diretamente (ex: $2^2=4$ , propriedades de números pares/ímpares) ou após algumas iterações de correção de erro (ex: lemas de simplificação).
- Para o lema mais complexo, evenpp:evenp (provando que se o quadrado de um número é par, o próprio número é par), o LLM falhou inicialmente. Os autores forneceram uma dica em linguagem natural delineando a prova por casos (par vs. ímpar), após a qual o LLM gerou com sucesso a prova formal.
- O teorema principal (sqrt2:irrational) exigiu que os autores fornecessem o esqueleto da prova; o LLM então preencheu os passos necessários e os lemas auxiliares.
Comparação com ATP: Embora os ATPs pudessem provar 9 de 12 lemas na versão final, eles falharam em provar o teorema principal dentro do tempo limite de 20 segundos, provavelmente devido ao espaço de busca expandido. Crucialmente, as provas de ATP não podiam ser convertidas diretamente nas provas de dedução natural exigidas pelo LPTP.
Gestão de Dependências: O artigo detalha o grafo de dependência dos lemas, mostrando como a capacidade do LLM de provar propriedades simples (como nat:natsquare ou sqr2:4) foi essencial para provar propriedades de nível superior.

Significância e Alegações
Os autores afirmam que este trabalho representa uma das primeiras interações entre o LPTP e um LLM. Sua principal contribuição é demonstrar um fluxo de trabalho semiautomático onde:

O Verificador de Provas é Central: O verificador LPTP atua como o filtro crítico contra alucinações do LLM. Ele fornece feedback preciso (o primeiro passo incorreto), permitindo que o LLM se autocorrija de forma eficaz.
Papéis Complementares: Os ATPs são rápidos e locais, mas produzem provas em um formato (resolução/superposição) incompatível com a dedução natural do LPTP. Os LLMs, guiados pelo verificador, podem gerar provas no formato correto, embora requeiram orientação humana para etapas estruturais complexas.
Viabilidade para LP: O estudo valida que os LLMs podem ser efetivamente integrados na verificação de propriedades de Programação Lógica, desde que haja um ciclo rigoroso de verificação de provas em vigor.

O artigo conclui modestamente, observando que, embora o LLM não pudesse gerar toda a estrutura da prova de forma autônoma para o teorema principal, ele lidou com sucesso com os passos lógicos granulares uma vez que a estrutura foi definida. Isso abre caminho para futuras abordagens potencializadas por IA na prova de propriedades de Prolog, com os autores planejando avaliar esta combinação em um conjunto mais amplo de problemas de verificação.

A Grande Parceria de Verificação de Provas

Os Resultados: Uma Vitória Parcial

O Que Isto Significa

Mais como este