A Axiom Math informou em 26 de outubro que concluiu o que descreve como a primeira prova completa da Classificação dos Grupos Simples Finitos verificada por computador no Lean.
No anúncio da Axiom Math, a empresa afirma que o projeto formalizou a prova CFSG de primeira geração e a reduziu a etapas que o Lean podia verificar mecanicamente. A Axiom também diz que o trabalho durou 24 dias, usou dezenas de agentes de IA e gerou cerca de 43.1 milhões de linhas de código Lean.
A formalização fez mais do que reproduzir a literatura. A Axiom afirma que identificou 34 divergências relevantes em relação aos argumentos publicados e sinalizou um problema em uma abordagem publicada para o Teorema do Grupo Desbalanceado. A empresa diz que planeja publicar uma lista de erratas mais longa para matemáticos.
Para quem desenvolve, a parte mais interessante é menos o teorema em si do que o modelo operacional: dividir um problema com muitas dependências em subproblemas rastreados e manter um verificador no ciclo para que resultados plausíveis não sejam confundidos com um resultado concluído. Esse padrão é relevante onde agentes precisam comprovar cobertura e correção, não apenas produzir texto que parece completo.