A matemática sempre dependeu de duas linguagens distintas. Uma é a linguagem natural que usamos para explicar ideias, contar histórias e compartilhar percepções; ela é flexível, rica em contexto e frequentemente pula etapas que parecem óbvias para um leitor humano. A outra é a linguagem formal dos assistentes de prova, sistemas computacionais rígidos que verificam cada movimento lógico para garantir que uma conclusão seja indubitavelmente verdadeira. Por décadas, pesquisadores trabalharam para traduzir a primeira linguagem na segunda, um processo chamado autoformalização. O objetivo era simples: pegar uma prova escrita por um humano e transformá-la em código que um computador possa verificar. Mas um problema crítico permanecia. Um computador frequentemente conseguia produzir uma prova que era tecnicamente correta, mas que não guardava semelhança com o argumento humano que a inspirou. O computador poderia resolver o problema usando um caminho completamente diferente, escondendo o raciocínio original atrás de uma parede de atalhos automatizados. Isso criava um abismo entre a verdade e a compreensão. Se a prova do computador não segue os passos do humano, não podemos usar essa prova para verificar se o raciocínio do humano foi realmente sólido, nem podemos confiar nela para nos ensinar como o argumento funciona.

Uma equipe de pesquisadores abordou agora esse abismo com um novo sistema projetado para manter a prova do computador fiel ao processo de pensamento original do humano. Eles chamam seu sistema de Pistis, um nome derivado da palavra grega antiga para fé ou confiança. Os pesquisadores aplicaram este sistema aos três primeiros livros dos Elementos de Euclides, um texto fundamental de geometria escrito há mais de dois mil anos. O trabalho deles demonstra que é possível traduzir esses argumentos antigos para uma linguagem de computador moderna sem perder a lógica original, ao mesmo tempo em que revela erros ocultos no texto que passaram despercebidos por séculos.

O desafio central que a equipe enfrentou foi que a linguagem natural e a lógica computacional operam em ritmos diferentes. Uma prova humana pode dizer: "Vamos assumir que isto é verdadeiro", e seguir em frente, esperando que o leitor preencha a lacuna. Um computador, no entanto, exige que cada etapa seja explicitamente declarada e justificada. Tentativas anteriores de traduzir provas frequentemente permitiam que o computador preenchesse essas lacunas com sua própria lógica, efetivamente reescrevendo o argumento para tornar mais fácil a resolução pela máquina. O resultado era uma prova que compilava com sucesso, mas falhava em refletir a intenção do autor humano. Pistis foi construído para prevenir isso. Em vez de pedir ao computador que encontre qualquer maneira possível de provar a afirmação, o sistema força o computador a seguir o caminho específico do humano, frase por frase.

Para alcançar isso, os pesquisadores desenvolveram um método que divide o processo de tradução em duas fases distintas. Primeiro, uma fase de mapeamento analisa o texto em linguagem natural e o divide em uma sequência de etapas pequenas e atômicas. Ela identifica exatamente o que cada frase afirma e em quais suposições ela se baseia. Isso cria um modelo estrito que o computador deve seguir. Segundo, uma fase de preenchimento tenta provar cada uma dessas pequenas etapas individualmente. O sistema utiliza uma estratégia de busca especializada que impede o computador de tomar atalhos ou saltar etapas. Se o computador não consegue provar uma etapa específica usando exatamente as ferramentas e referências mencionadas no texto humano, ele não simplesmente encontra uma forma diferente de resolver o problema. Em vez disso, ele sinaliza o problema, revelando que o argumento humano original pode ter um buraco ou uma peça faltante.

Essa abordagem provou ser notavelmente eficaz quando testada na geometria de Euclides. Os pesquisadores geraram provas formais para 92 proposições ao longo dos três primeiros livros. Quando compararam essas novas provas com tentativas anteriores, a diferença foi gritante. As novas provas compilaram mais de trinta e três vezes mais rápido, uma melhoria significativa na eficiência que sugere que o novo método evita as computações pesadas e lentas de sistemas antigos. Mais importante ainda, especialistas humanos que revisaram as provas preferiram a saída do novo sistema por uma margem larga. Em um estudo cego, os revisores consideraram as novas provas muito mais transparentes e melhores representações dos argumentos do livro didático original. Um juiz de inteligência artificial, treinado para avaliar a qualidade da tradução, concordou, favorecendo as novas provas sobre as antigas em uma proporção de mais de cinco para um.

Além de simplesmente traduzir o texto, o sistema atuou como um verificador rigoroso que expôs falhas genuínas no material de origem. Por insistir em seguir a lógica humana exatamente, o sistema não consegue esconder erros. Em um caso, o sistema identificou um erro de citação em uma tradução moderna de Euclides. O texto referenciava uma proposição sobre cortar uma linha ao meio, mas a citação apontava para uma proposição sobre cortar um ângulo. O sistema sinalizou essa incompatibilidade, mostrando que a tradução havia vinculado a ideia errada ao passo errado. Em outro caso, o sistema encontrou uma lacuna no próprio raciocínio de Euclides, onde um cenário específico foi deixado sem tratamento. Os pesquisadores foram capazes de demonstrar formalmente que o argumento original era incompleto, uma descoberta que teria sido difícil de fazer sem uma ferramenta que adere estritamente à estrutura original.

O sucesso de Pistis sugere que a formalização fiel não é apenas um exercício técnico, mas uma ferramenta poderosa para verificar o conhecimento humano. Ao forçar o computador a percorrer o mesmo caminho que o humano, o sistema pode confirmar se o raciocínio se sustenta ou onde ele falha. Os pesquisadores descobriram que seu método podia aceitar argumentos válidos, refutar argumentos inválidos e apontar exatamente onde uma prova deu errado. Essa capacidade estende-se além da geometria antiga; a estrutura foi projetada para funcionar com qualquer argumento matemático escrito em linguagem natural. O trabalho mostra que não temos que escolher entre a flexibilidade da explicação humana e o rigor da verificação de máquina. É possível ter ambos, desde que a máquina seja guiada para respeitar a voz e a lógica originais do humano.

O estudo também destacou os limites da tecnologia atual. Embora o sistema tenha funcionado bem para os três primeiros livros de Euclides, ele não conseguiu lidar com todas as proposições dos livros posteriores sem orientação humana adicional. Algumas proposições exigiam conceitos geométricos que o sistema computacional subjacente ainda não sabia como lidar, como medir o comprimento de uma linha curva. Os pesquisadores observaram que seu sistema depende de um humano ou de uma inteligência artificial avançada para atuar como um oráculo, verificando se o mapeamento inicial do texto está correto. Isso significa que o processo ainda não é totalmente automático, mas reduz significativamente a quantidade de trabalho manual necessário em comparação com métodos anteriores.

Em última análise, o artigo apresenta um novo padrão para como interagimos com provas matemáticas na era da inteligência artificial. Ele vai além da questão de se um computador pode provar um teorema para a questão mais profunda de se o computador entende o argumento. Ao garantir que a prova formal espelhe o argumento em linguagem natural passo a passo, os pesquisadores criaram uma ferramenta que pode validar o raciocínio por trás de uma conclusão, não apenas a conclusão em si. Isso permite que matemáticos e estudantes confiem que o computador não está apenas encontrando uma solução, mas está verdadeiramente seguindo a lógica da pessoa que escreveu a prova. O trabalho oferece um caminho a seguir onde o insight humano e a precisão da máquina trabalham juntos, preservando a integridade da descoberta matemática enquanto aproveitam o poder da verificação moderna.