A inteligência artificial superou uma das barreiras mais persistentes da matemática computacional. Um novo sistema chamado LeanMarathon formalizou completamente sete teoremas extraídos de quatro problemas do matemático Paul Erdős, provando 258 lemas e teoremas sem cometer nenhum erro.
O feito foi documentado em artigo submetido ao repositório científico arXiv e representa um salto qualitativo em relação às tentativas anteriores de usar IA para verificar demonstrações matemáticas. Diferentemente dos sistemas que funcionam bem em provas curtas, mas se degradam em projetos longos, o LeanMarathon mantém a fidelidade do raciocínio do início ao fim do desenvolvimento.
A arquitetura do sistema se apoia em quatro agentes especializados com funções bem definidas. Um agente constrói o arcabouço formal, outro audita a precisão lógica, um terceiro se encarrega das demonstrações e o quarto repara inconsistências que surgem durante o processo. Esses agentes operam sobre o que os pesquisadores chamam de ‘blueprint’ — um arquivo que funciona simultaneamente como esqueleto da prova formal, grafo de raciocínio em linguagem natural e registro compartilhado do sistema.
Um orquestrador de dois estágios coordena o trabalho. Primeiro, estabiliza a correspondência entre o teorema original e sua versão formalizada por meio de revisão adversarial. Depois, percorre o grafo de dependências das demonstrações das folhas dinâmicas para cima em rodadas paralelas. Os testes foram realizados em três execuções autônomas completas sobre artigos recentes de pesquisa matemática. Em todas elas, o LeanMarathon alcançou o objetivo máximo da formalização matemática: zero ‘sorry’ — termo usado no assistente de provas Lean para indicar lacunas não preenchidas na demonstração. Isso significa que todos os 258 lemas e teoremas foram rigorosamente verificados pela máquina, sem exceção.
O avanço resolve um problema descrito pelos autores como ‘decadência de contexto’ — fenômeno em que as declarações matemáticas se desviam sutilmente do significado original, as dependências se enroscam e reparos locais corrompem demonstrações já concluídas em outras partes do projeto. Ao transformar uma única execução frágil de várias horas em muitas transações locais, recuperáveis e paralelas, o sistema impede que o colapso se propague.
A pesquisa demonstra que a construção de co-matemáticos artificiais confiáveis exige não apenas provadores mais potentes, mas também arcabouços duráveis que preservem a fidelidade dos teoremas ao longo de desenvolvimentos matemáticos extensos. O código do LeanMarathon está disponível publicamente, permitindo que outros grupos de pesquisa repliquem e ampliem os resultados. O sucesso na formalização dos problemas de Erdős — numerados 1051, 1196, 164 e 1217 — sinaliza um horizonte em que a IA poderá atuar como parceira verificadora em todas as frentes da matemática avançada. A combinação de agentes especializados com orquestração inteligente pode se tornar o padrão para qualquer sistema que exija raciocínio lógico de longo alcance.
Nenhum comentário ainda, seja o primeiro!