OpenAI publica no GitHub 722 trabalhos de matemática escritos por um modelo fechado

A OpenAI publicou no GitHub, há alguns dias, 722 trabalhos de matemática gerados por um modelo frontier interno que ainda não foi lançado. Os temas são teoria dos números, geometria algébrica, análise e combinatória. Parte dos resultados vem acompanhada de provas formais em Lean. O veículo chinês Jiqizhixin descreve as consequências em tom duro: a IA começou a produzir matemática nova mais rápido do que os matemáticos conseguem compreendê-la, e a comunidade vai precisar de anos para digerir tudo isso.

O que exatamente foi publicado

A escala chama a atenção. Mais de setecentos trabalhos em um único pacote, cobrindo várias áreas da matemática ao mesmo tempo. Normalmente, um volume desses leva anos e dezenas de autores para se acumular.

O trecho disponível do material termina na descrição do repositório. Por isso, vários detalhes importantes são desconhecidos: como os arquivos estão organizados, sob qual licença os textos foram publicados, quantas pessoas participaram da seleção e se os trabalhos passaram por revisão por pares. A OpenAI não lançou o modelo, e não é possível reproduzir o resultado de fora.

• 722 trabalhos em um repositório aberto no GitHub
• Fonte: modelo interno não publicado da OpenAI
• Áreas: teoria dos números, geometria algébrica, análise, combinatória
• Parte dos trabalhos tem verificação formal em Lean
• Status de avaliação independente: não informado no material disponível

O gargalo se deslocou para a verificação

O Lean funciona aqui como uma garantia. É um sistema de provas em que um compilador verifica cada passo. Se a prova compila, não há lacunas lógicas nela. Mas sobram perguntas que a máquina não resolve. O enunciado formalizado é exatamente o que o artigo afirma? O resultado é interessante, ou é apenas um corolário secundário de algo já conhecido? Ele se encaixa em uma linha de pesquisa ativa?

Para os trabalhos sem formalização, o quadro é pior. Quem os lê é uma pessoa, e a revisão de um único artigo complexo leva semanas, às vezes meses. Com 722 textos, essa fila vira um problema que não se resolve contratando alguns revisores a mais.

A segunda parte da manchete do Jiqizhixin diz que os matemáticos ficaram sem projetos de pesquisa: “os projetos de pesquisa desapareceram”. O mecanismo é simples. Se o modelo resolve um problema em que um doutorando pretendia trabalhar por um ano e meio, o tema perde valor antes de ele conseguir defender a tese. Essa é uma avaliação do veículo, e não um fato confirmado sobre pessoas específicas, mas a lógica é clara. Correm mais risco os que trabalham com problemas técnicos e fáceis de formalizar.

Como lidar com isso

Os matemáticos devem comparar seus temas atuais com o repositório. É melhor encontrar sobreposições agora do que depois de enviar um preprint. Também vale aprender Lean, ao menos o suficiente para ler: a capacidade de verificar rapidamente a formalização de outra pessoa está virando uma habilidade de trabalho.

Revistas científicas e plataformas como o arXiv terão de definir uma política. Aceitar ou não textos escritos por um modelo, e exigir ou não uma prova formal como condição para análise. Sem isso, o fluxo de trabalhos feitos por máquina simplesmente vai entupir a fila.

Para engenheiros e líderes de equipe, a lição é mais ampla. A verificação formal está saindo do nicho acadêmico e se tornando uma forma de aceitar resultados de IA sem confiar na palavra do modelo. O mesmo princípio vale para código e sistemas críticos.

Por fim, enquanto não houver análises independentes, é prudente evitar conclusões enfáticas. O principal indicador para os próximos meses: que parcela dos 722 trabalhos vai resistir à verificação e quantos se mostrarão substanciais, e não apenas corretos.