# Axiom transforma o Stacks Project em código Lean verificado

> Axiom afirma que sua formalização, com 16 milhões de linhas, torna uma importante referência de geometria algébrica reutilizável em provas verificadas pelo Lean.

Oossa · 2026-11-05 · https://oossa.com/pt/axiom-turns-the-stacks-project-into-machine-checked-lean-code

A Axiom Math lançou uma versão verificada por máquina do Stacks Project, uma importante referência de código aberto em geometria algébrica. A formalização traduz a matemática do projeto em cerca de 16 milhões de linhas de código Lean, verificadas passo a passo por um programa de checagem de provas. Segundo a Axiom, pesquisadores e agentes de IA podem usar os resultados como uma biblioteca integrada para desenvolver novas provas formais.

As fontes apresentam números ligeiramente diferentes de páginas: a TechCrunch informa cerca de 7.654 páginas, enquanto a Axiom descreve o projeto como tendo aproximadamente 7.500. A referência original foi iniciada em 2005 pelo matemático Johan de Jong, da Universidade Columbia, e ampliada por matemáticos ao longo de duas décadas. O trabalho da Axiom formaliza esse conhecimento já existente; não significa que os agentes de IA tenham descoberto a matemática subjacente por conta própria.

## Por que uma biblioteca integrada é importante?

Uma biblioteca de provas é útil não apenas porque seus teoremas foram verificados individualmente, mas também porque provas posteriores podem reutilizá-los e aproveitar suas dependências. A Axiom afirma ter preservado as etiquetas permanentes do Stacks Project, ligando as declarações em Lean às partes correspondentes do texto original. Em seu site, a empresa também permite que os leitores vejam o texto e o código lado a lado e explorem as dependências entre os resultados.

Isso é especialmente importante na geometria algébrica, em que uma prova pode depender de uma longa cadeia de ideias de áreas como álgebra comutativa, esquemas, feixes e cohomologia. A Axiom diz que, antes desse lançamento, os pesquisadores dispunham de uma infraestrutura Lean bem mais limitada para formalizar a geometria algébrica moderna. A biblioteca da empresa oferece um ponto de partida, sem exigir que esses fundamentos sejam formalizados novamente em cada projeto.

## Uma base para futuras provas — e softwares

Segundo a Axiom, seus agentes trabalharam em paralelo para traduzir, provar e integrar milhares de teoremas. A TechCrunch informa que a empresa forneceu aos agentes uma estrutura flexível para que identificassem tarefas e trabalhassem nelas, e que a Axiom também treinou seus próprios modelos especializados em matemática. A empresa afirma que a biblioteca concluída é a maior biblioteca integrada e reutilizável de matemática formalizada; essa é a caracterização da Axiom para o lançamento.

O mesmo tipo de verificação é usado em áreas como projeto de chips e validação de software. A Axiom argumenta que fundamentos verificados e reutilizáveis podem ajudar agentes de IA a criar sistemas mais confiáveis à medida que escrevem mais código. Mas o lançamento verifica a formalização do Stacks Project, não toda nova afirmação matemática ou todo software que um sistema de IA possa produzir.

## Os fatos

- A Axiom datou o lançamento de 4 de novembro de 2026.
- A formalização em Lean contém cerca de 16 milhões de linhas de código.
- O Stacks Project foi iniciado por Johan de Jong em 2005 e cresceu com contribuições de matemáticos.
- Segundo a TechCrunch, a Axiom captou US$ 200 milhões em uma rodada Série A liderada pela Menlo Ventures em março de 2026.

## Por que importa

Para matemáticos que trabalham com geometria algébrica, a biblioteca oferece resultados verificados que podem ser reutilizados, em vez de reconstruir os mesmos fundamentos em Lean. Ela confirma a formalização dessa referência, mas não garante que futuras provas ou códigos gerados por IA sejam confiáveis sem verificação.

## Fontes e referências

1. [Axiom Math wants to keep AI slop out of mathematics](https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/) – TechCrunch, 2026-11-05
2. [Axiom](https://axiommath.ai/research/the-stacks-project-formalized/?utm_source=openai) – Axiom

Última atualização: 2026-11-05