Axiom Math verificou 16 milhões de linhas de código Lean com agentes e fechou uma lacuna na matemática formal

Quando a IA «resolve» um novo problema matemático toda semana, surge uma pergunta razoável: quem verifica tudo isso? Só no mês passado, a OpenAI divulgou 719 manuscritos com supostas soluções para problemas difíceis. Ler todos à mão é impossível, e erros passam mesmo com verificações automáticas. A Axiom Math, startup avaliada em US$ 1,6 bilhão, propõe outro caminho: não desacelerar, mas se apoiar em uma base verificada.

O que exatamente foi feito

Na quarta-feira, a empresa anunciou que verificou formalmente o Stacks Project, uma das maiores coletâneas de matemática humana da história. Ele foi iniciado em 2005 por Johan de Jong, da Universidade Columbia, como uma referência aberta. Hoje tem cerca de 7654 páginas: da álgebra universitária a ideias de ponta em geometria algébrica e teoria dos números.

Os agentes da Axiom reescreveram tudo isso em cerca de 16 milhões de linhas de código na linguagem Lean. Depois, um programa chamado proof assistant verificou o código linha por linha. Se a verificação passa, a demonstração é logicamente correta e não é preciso acreditar na palavra do autor.

Por que é mais difícil do que parece

Verificar cada teorema isoladamente é apenas metade do trabalho. Os resultados do Stacks Project estão ligados como uma árvore genealógica: cada um se apoia nos anteriores. Se uma definição «escorrega» em algum ponto, tudo o que está acima desmorona. Por isso, a equipe precisou preservar todas as conexões ao longo de 16 milhões de linhas. A própria CEO, Carina Hong, admite que no início não tinha certeza do sucesso: o grande e o frágil combinam mal.

A arquitetura foi esta: uma hierarquia flexível no topo, mas sem distribuição rígida de tarefas. Os agentes encontravam por conta própria no que trabalhar e atuavam em paralelo. A Axiom também treinou modelos próprios para matemática, algo que, segundo Hong, a maioria dos concorrentes em verificação não faz. No início, um especialista interno em Lean incutiu nos agentes «bom gosto», isto é, a compreensão de como deve ser um bom código. Com o tempo, diz Hong, eles passaram a se virar sozinhos.

Por que isso importa para desenvolvedores

O sentido prático não está na geometria algébrica em si. A verificação formal há muito é usada onde o erro sai caro: a verificação de chips, e pesquisadores franceses a usaram para encontrar bugs em um software que calcula benefícios familiares. O problema é que os agentes escrevem cada vez mais código, sem que aumentem as garantias de ausência de bugs e falhas de segurança.

A aposta da Axiom: a matemática é um campo de provas onde essa habilidade é aperfeiçoada e depois transferida para o software. Os agentes podem ler uma biblioteca Lean pronta e construir sobre ela sem começar do zero. Terence Tao formula o princípio geral assim: quanto mais demonstrações formalizadas existirem, mais coisas novas poderão ser feitas.

Limitações

Por enquanto, trata-se de uma declaração da própria empresa, e o material não traz avaliação independente do resultado. Transferir a habilidade da matemática para o código industrial é uma hipótese, não um fato comprovado. O software real depende do ambiente, das dependências e de requisitos informais que não se formalizam tão limpamente quanto teoremas. O desafio de Hong a todas as empresas que escrevem código para que formalizem nessa escala soa ousado, mas por ora é mais marketing.

O que fazer na prática

Se você constrói sistemas de agentes para código, dê uma olhada no Lean e na ideia de artefatos verificáveis: faça o agente entregar não só código, mas também algo que seja verificado automaticamente. Para as equipes de produto, a conclusão é mais simples: «a IA escreveu» e «a IA escreveu e está provado» logo serão duas categorias distintas de qualidade. Quem atua em áreas críticas, como finanças, medicina e segurança, deve manter essa mudança no radar desde já.