SAT prova menor contraexemplo para problema de Tarski

O que aconteceu

Um grupo de pesquisadores, liderado por Bernardo Anibal Subercaseaux Roa, publicou no arXiv (em 9 de agosto de 2026) o artigo "A SAT Attack on Tarski's High School Algebra Problem". Usando solvers SAT, eles provaram que o menor contraexemplo ao problema de Tarski — que pergunta se toda identidade verdadeira sobre adição, multiplicação e exponenciação de inteiros positivos segue de 11 axiomas elementares — tem exatamente 12 elementos. Isso confirma a conjectura de Burris e Yeats, que em 2010 haviam encontrado um contraexemplo de tamanho 12, mas não provaram minimalidade. O artigo mostra ainda que existem exatamente 8.957.952 contraexemplos de tamanho 12 (a menos de isomorfismo) e os classifica de forma simples.

Contexto

O problema de Tarski foi proposto pelo lógico Alfred Tarski na década de 1960. Em 1981, Wilkie exibiu uma identidade válida sobre inteiros positivos que não pode ser derivada dos 11 axiomas de Tarski. Gurevič construiu uma álgebra de 59 elementos que satisfaz os axiomas mas viola a identidade de Wilkie. Ao longo dos anos, diversos autores reduziram o tamanho do contraexemplo, chegando a 12 elementos com Burris e Yeats. Zhang provou que não há contraexemplo com menos de 11 elementos. A lacuna entre 11 e 12 permaneceu em aberto por mais de uma década.

Por que importa

A prova por SAT é significativa porque mostra que solvers SAT podem resolver problemas matemáticos abertos que ferramentas dedicadas (como Mace4 e SEM) não conseguem atacar com eficiência. O artigo relata que a abordagem SAT superou essas ferramentas na busca por contraexemplos em teorias equacionais. Além disso, o uso de autoformalização no provador Lean garante a correção do resultado principal, um passo importante para a verificação formal de provas assistidas por computador.

Impacto

No curto prazo, o resultado fecha uma conjectura de 15 anos e fornece uma classificação completa dos contraexemplos mínimos. Isso pode levar a novos insights sobre a estrutura das álgebras que satisfazem os axiomas de Tarski. No médio prazo, a técnica de usar SAT para explorar espaços de modelos finitos pode ser aplicada a outros problemas em lógica e álgebra universal. A combinação com Lean também reforça a tendência de usar provadores interativos para validar resultados gerados por ferramentas automáticas.

O que muda

O problema de Tarski, que era um exemplo clássico de um teorema verdadeiro mas não demonstrável a partir de um conjunto finito de axiomas, agora tem uma compreensão mais completa: os contraexemplos mínimos têm exatamente 12 elementos. Isso não altera a resposta original de Wilkie, mas refina o entendimento da fronteira entre o que é demonstrável e o que é verdadeiro. Para a comunidade de SAT, o artigo demonstra que solvers podem ser usados como ferramentas de descoberta matemática, não apenas para verificação.

O que vem agora

Os autores pretendem disponibilizar o código e os dados da classificação. A comunidade pode explorar se a técnica se estende a outros problemas de álgebra universal. Também é possível que a classificação dos 8,9 milhões de contraexemplos revele padrões que levem a uma prova humana mais elegante da minimalidade. O artigo está disponível no arXiv (2608.08421) e gerou discussão no Hacker News.