O maior projeto de prova da matemática moderna acaba de passar por sua primeira auditoria séria por máquina. Em sete meses, um fluxo de trabalho impulsionado por IA chamado FormaTheoria escreveu mais de 994.000 linhas de código Lean para formalizar quatro teoremas fundamentais da Classificação dos Grupos Finitos Simples (CFSG) — o monumental esforço de prova que se estende por cerca de 20.000 páginas em centenas de artigos, construído por centenas de matemáticos ao longo de décadas.
Os quatro teoremas — o teorema da ordem ímpar de Feit–Thompson, o teorema Z* de Glauberman, o teorema de Brauer–Suzuki e o teorema de Bender–Suzuki — formam uma cadeia conectada no coração da classificação. Para dar uma ideia da escala: uma formalização anterior de apenas o teorema de Feit–Thompson, feita no assistente de provas Rocq (Coq), levou cerca de 15 pessoas durante seis anos. A FormaTheoria completou esse volume de trabalho em sete meses e ainda o estendeu.
Esse é o título da notícia. A história mais interessante é como o sistema conseguiu isso, porque a engenharia por trás se generaliza muito além da matemática.
Não é uma IA que resolve problemas prontos
A maioria dos sistemas de IA matemática recebe um enunciado limpo, com definições e ferramentas já montadas, e então busca uma prova. A FormaTheoria funciona de forma diferente. Ela parte da literatura bruta e bagunçada e precisa primeiro reconstruir os fundamentos matemáticos por baixo do teorema — lendo livros, resolvendo dependências, conciliando notações — antes de construir a prova formal e submeter cada passo ao assistente de provas Lean. O projeto foi iniciado sob o incentivo de Shing-Tung Yau, com estudantes do Qiuzhen College da Tsinghua, além de pesquisadores do Yau Mathematical Sciences Center, do Institute for AI Industry Research e da Universidade de Warwick.
Os autores descrevem quatro problemas difíceis, cada um com uma resposta de engenharia:
- Você não sabe quanta leitura será necessária. Uma citação leva a um artigo, que leva a mais pré-requisitos. O projeto começou com 3 fontes principais e descobriu 12 outras no meio da prova; 65,6% de todas as páginas consultadas foram adicionadas durante a própria prova. A resposta do sistema: quando um pré-requisito ausente aparece, pausa-se a prova, formaliza-se a dependência e retorna-se à tarefa. Cada resultado verificado é arquivado em uma base de conhecimento compartilhada para reutilização por teoremas futuros.
- Definições não se combinam entre artigos. Dois autores podem definir o “mesmo” conceito de maneiras diferentes — matematicamente equivalentes em prosa, incompatíveis quando escritos em Lean. O sistema constrói pontes de tradução explícitas entre as fontes e protege enunciados já verificados de danos colaterais durante reparos.
- Código que passa no Lean ainda pode interpretar mal o original. O Lean verifica se uma prova é autoconsistente e se a conclusão decorre das premissas. Ele não verifica se a conclusão representa fielmente o artigo. A IA pode omitir uma condição, confundir “todo” com “existe” ou modificar silenciosamente uma conclusão. A resposta é um estágio dedicado de revisão independente: um componente tradutor escreve o enunciado em Lean, e um componente revisor o reconfere linha por linha contra a fonte. Das 14 seções da literatura analisadas, 11 traduções de primeiro rascunho foram devolvidas para revisão. É essa segunda barreira que separa “verificado por máquina” de “mal interpretado por máquina”.
- A literatura original às vezes está simplesmente errada. Artigos antigos contêm erros de digitação, hipóteses faltantes e formulações ambíguas. O sistema detectou duas definições incompatíveis de “subgrupo maximal do tipo I” entre as fontes e as conciliou usando o teorema de Schur–Zassenhaus; sinalizou um lema de Péterfalvi sem a precondição de ordem ímpar; encontrou um teorema em Huppert com uma condição de divisibilidade errada, produziu um contraexemplo e escalou a questão para matemáticos humanos, que confirmaram a condição correta. Até um simples erro de digitação sobreviveu em ambos os livros de referência — o objeto H escrito como M ao longo do texto.
A engenharia de longo prazo importa tanto quanto o raciocínio em si. Um “mapa de prova” constantemente atualizado divide objetivos difíceis em lemas, incorpora resultados bem-sucedidos aos teoremas principais e registra caminhos fracassados para que o sistema não caia repetidamente nos mesmos becos sem saída. O paralelismo consciente das dependências calcula pré-requisitos compartilhados apenas uma vez para cada consumidor (um ganho de velocidade de 4,2× nas tarefas testadas). A execução contínua mais longa de um agente durou 9,17 dias, durante os quais o sistema realizou 606 passagens de compressão de memória, mantendo vivos o objetivo atual, os resultados completados e as questões em aberto.
Os números finais: 30.298 enunciados matemáticos e 186.187 arestas de dependência na rede de provas, com a cadeia de dependências mais longa alcançando 458 camadas. Contando a biblioteca padrão do Lean, a rede cresce para 74.922 enunciados e mais de 1,44 milhão de dependências.
A moldura útil: artigos de matemática são uma base de código legada sem documentação
A CFSG são 20.000 páginas de prosa escritas por centenas de autores ao longo de décadas, com convenções que “os leitores da área conhecem”. Nenhum compilador jamais verificou nada disso. Os erros se escondem à vista de todos porque leitores competentes os corrigem silenciosamente durante a leitura.
A verificação formal é o compilador que a matemática nunca teve. Cada definição, cada condição, cada inferência precisa ser explícita. O trabalho da IA não era “escrever uma prova” — era reconstruir todo o grafo de dependências de um sistema de 20.000 páginas e fazê-lo passar na checagem de tipos. A verificação é o resultado visível; o verdadeiro ativo é a infraestrutura reconstruída e auditável por baixo.
Para quem já trabalhou com sistemas legados, a analogia é precisa. Artigos de matemática são uma base de código sem testes que todos têm medo de refatorar. O mapa de prova é um issue tracker. A passagem do revisor é uma code review. Escalar para os matemáticos é um processo de incidentes. A novidade não é a gestão — é que um agente de IA agora conduz toda a operação.
Por que isso importa além da matemática
Primeiro, o limite de capacidade se move. A IA não está mais limitada a resolver problemas preparados e isolados. Ela agora pode manter e estender uma grande infraestrutura de conhecimento de longo prazo — rodando por dias, comprimindo contexto, rastreando dependências através de dezenas de fontes e mantendo uma thread de várias semanas coerente. Essa é uma capacidade de agente, e ela se generaliza para qualquer domínio com grandes corpos de conhecimento interconectados.
Segundo, o padrão de verificação é um modelo para IA confiável. Note as três camadas: um verificador que prova consistência interna (Lean), um revisor independente que checa a fidelidade em relação à fonte da verdade e um caminho de escalonamento humano quando as evidências são insuficientes. IA corporativa que gera código, contratos ou alegações científicas precisa exatamente dessa separação. O gerador pode ser fluente; o verificador deve ser adversarial; o humano detém o julgamento.
Terceiro, a matemática verificada se torna um ativo reutilizável. A rede formalizada servirá como infraestrutura para teoremas futuros, do mesmo modo que uma biblioteca bem testada é infraestrutura para softwares futuros. Quando ferramentas de busca, explicação e visualização forem acopladas, os pesquisadores consultarão essa rede em vez de rederivá-la manualmente.
Quarto, esta é a versão funcional da colaboração humano-máquina. Os humanos decidem quais problemas valem a pena resolver e fazem os julgamentos-chave; a IA executa a busca e a derivação em grande escala; os sistemas formais garantem que cada passo aceito possa ser re-verificado. Quando uma prova é grande demais para qualquer indivíduo reler, essa divisão de trabalho não é uma escolha — é a única opção.
O que você pode levar daqui
- Se você constrói agentes de longa duração, gerencie-os como a FormaTheoria: um mapa de progresso persistente, caminhos fracassados registrados, memória comprimida e dependências compartilhadas calculadas exatamente uma vez.
- Se você entrega código ou afirmações gerados por IA, adicione uma checagem independente de fidelidade em relação à sua fonte da verdade. Passar no verificador não é o mesmo que ser fiel — 11 dos 14 primeiros rascunhos foram rejeitados pela revisão neste projeto.
- Não trate “verificado por máquina” como sinônimo de “entendido por máquina”. Ferramentas de verificação garantem consistência interna, não correspondência com a intenção. Você precisa das duas camadas, ou terá rigor sem verdade.
Artigo: arXiv:2608.10894 · Código: github.com/Qiuzhen-CFSG/CFSG
