← Artigos
Math Inc. e o agente Gauss: IA formaliza teorema dos números primos em Lean
Por Luis Eduardo da Cruz4 min de leituraInteligência Artificial
A Math Inc., startup californiana, desenvolveu um agente de IA chamado Gauss que, em apenas três semanas e sem ajuda humana significativa, formalizou em código Lean um dos teoremas mais importantes da teoria dos números — o teorema dos números primos, provado em 1896.
O resultado: 25 mil linhas de código com mais de mil teoremas auxiliares, num processo que projetos anteriores levavam décadas para completar.
O objetivo é criar agentes cada vez mais autônomos capazes de verificar, com rigor matemático total, se raciocínios e provas estão realmente corretos.
Matemática formalizada?
Perguntas frequentes
- O que o agente Gauss da Math Inc. fez?
- Formalizou em código Lean o teorema dos números primos, provado em 1896, em cerca de três semanas e sem ajuda humana significativa.
- Qual foi a escala do resultado?
- Cerca de 25 mil linhas de código e mais de mil teoremas auxiliares — um trabalho que, em projetos anteriores de formalização, levava décadas.
- Por que matemática formalizada importa para a IA?
- Porque permite verificar com rigor total se raciocínios e provas estão corretos, abrindo caminho para agentes autônomos confiáveis em ciência e engenharia.