Segundo relatos sobre a mais nova família de modelos da OpenAI, provisoriamente chamada Astra, essa nova geração será especializada em tarefas de médio a longo prazo que levam várias horas ou dias para serem concluídas. A ideia é complementar a linha existente de Sol, Terra e Luna, e não substituí-la. Sam Altman passou esta semana apresentando os novos modelos a legisladores em Washington.

Para demonstrar as capacidades do Astra na resolução de problemas complexos, a OpenAI publicou uma publicação neste sábado com soluções para 10 problemas de ciência da computação e matemática, a maioria dos quais permanecia em aberto havia anos. A empresa afirma que essas soluções foram produzidas por uma versão interna do Astra durante os testes.

O custo total estimado em tokens desses resultados ficou na casa de $2,000, segundo a empresa, calculado com base nas tarifas de API de seu atual modelo principal, GPT-5.6 Sol. A empresa acrescentou que "atribuir autoria humana a uma prova gerada inteiramente por um sistema de IA deturparia tanto a contribuição do sistema quanto a natureza do verdadeiro trabalho intelectual humano."

Isso ocorre porque anúncios anteriores de soluções matemáticas baseadas em IA foram publicados sob a autoria de humanos, com o modelo listado apenas como colaborador. No entanto, na publicação mais recente da OpenAI, o próprio modelo aparece como o principal solucionador do problema, enquanto os colaboradores humanos assumiram a responsabilidade pela preparação dos manuscritos.

Uma das soluções em questão — que resolveu um problema em uma área da álgebra abstrata chamada teoria dos grupos — vazou no X várias horas antes do anúncio oficial. Elliot Glazer, matemático-chefe da Epoch AI, rapidamente descreveu o trabalho como o resultado mais importante da IA em matemática até o momento.

O pesquisador de IA Sébastien Bubeck, que agora trabalha na OpenAI, brincou dizendo que esperava que a IA superasse suas habilidades matemáticas em 2030, e não em 2026.

Analisando as soluções do Astra

O resultado vazado primeiro no Twitter encerrou uma questão que estava em aberto desde que o matemático Benjamin Weiss cunhou o termo “sofic” no ano 2000. Em termos simples, um grupo matemático é um conjunto de movimentos mais uma regra para combiná-los, algo não muito diferente das rotações de um cubo mágico. Um grupo “sofic” é aquele em que, se você ampliar qualquer pequena parte do sistema, consegue construir uma versão finita que se comporta quase exatamente da mesma forma.

Até então, nenhum pesquisador havia conseguido identificar um grupo que não fosse sofic; todos os grupos conhecidos apresentavam a mesma propriedade. A revelação de sábado marcou o primeiro contraexemplo conhecido.

Os outros nove resultados abrangem outras áreas da matemática. Um deles refuta uma conjectura de longa data do matemático Alain Connes sobre o comportamento de determinadas estruturas matemáticas. Outro encontra uma resposta melhor para a questão de quão compactamente é possível empacotar esferas em espaços de dimensões muito altas, superando um recorde que permanecia de pé desde 1978.

Por que alguns são céticos em relação aos resultados da OpenAI

A OpenAI não é a única desenvolvedora de IA de fronteira a lançar seus modelos contra problemas matemáticos não resolvidos. O Claude Fable 5, desenvolvido pela Anthropic, teria identificado um contraexemplo que encerrou a Conjectura Jacobiana, de 87 anos, em três variáveis. O matemático da UCLA Terence Tao verificou publicamente o resultado em 21 de julho.

Afirmações anteriores da OpenAI sobre as capacidades matemáticas de seus modelos foram questionadas. A empresa atribuiu ao GPT-5.6 Sol Ultra, em 10 de julho, uma prova da Conjectura do Recobrimento Duplo de Ciclos — um problema matemático de longa data sobre a disposição de laços em uma rede. Os matemáticos Sang-il Oum e Jim Geelen escreveram críticas separadas a esse argumento, enquanto o Wolfram MathWorld registra que a afirmação não havia chegado a uma publicação revisada por pares até o fim do mês.

Alguns críticos também demonstraram ceticismo em relação a resultados anteriores de benchmarks divulgados pela própria empresa. No entanto, cada um dos resultados mais recentes veio acompanhado de um certificado Lean — uma prova escrita para verificação por computador — além dos manuscritos e das narrações do processo de raciocínio do modelo. Ainda assim, é importante observar que os resultados ainda não passaram pela revisão por pares convencional.