O modelo mais recente da OpenAI demonstrou uma capacidade inesperada na resolução de problemas matemáticos de alto nível, de acordo com testes conduzidos por engenheiro de software e ex-pesquisador quântico Neel Somani. Somani observou o modelo gerar uma solução completa após 15 minutos de processamento de um problema no ChatGPT, formalizando posteriormente a prova com a ferramenta Harmonic, confirmando sua precisão. Ele afirmou que pretendia estabelecer uma base para a capacidade dos grandes modelos de linguagem (LLMs) para resolver problemas matemáticos abertos. A cadeia de pensamento do modelo invocou axiomas matemáticos, incluindo a fórmula de Legendre, o postulado de Bertrand e o teorema da Estrela de David. Ele localizou uma postagem do Math Overflow de 2013 do matemático de Harvard Noam Elkies, que ofereceu uma solução de problema semelhante, mas a prova final do ChatGPT foi diferente e forneceu uma solução mais completa para uma versão de um problema colocado pelo matemático Paul Erdős. Desde o lançamento do GPT 5.2, que Somani descreveu como “anedóticamente mais hábil em raciocínio matemático do que as iterações anteriores”, um volume crescente de problemas resolvidos levantou questões sobre a capacidade dos LLMs de promover o conhecimento humano. Somani concentrou-se nos problemas de Erdős, uma coleção de mais de 1.000 conjecturas mantidas online, que variam em assunto e dificuldade. As primeiras soluções autônomas para esses problemas surgiram em novembro do AlphaEvolve, um modelo movido pelo Gemini. Mais recentemente, Somani e outros descobriram que o GPT 5.2 é adepto da matemática de alto nível. Desde dezembro, 15 problemas no site da Erdős passaram de “abertos” para “resolvidos”, com 11 soluções creditando modelos de IA. O matemático Terence Tao, em seu Página GitHubobservou oito problemas em que os modelos de IA fizeram progressos autónomos significativos e seis casos em que o progresso envolveu a localização e o desenvolvimento de pesquisas anteriores. Tao conjecturou no Mastodon que a natureza escalável dos sistemas de IA os torna “mais adequados para serem aplicados sistematicamente à 'cauda longa' de problemas obscuros de Erdős, muitos dos quais na verdade têm soluções diretas”, acrescentando que “muitos desses problemas mais fáceis de Erdős são agora mais prováveis de serem resolvidos por métodos puramente baseados em IA do que por meios humanos ou híbridos.” Uma força motriz neste avanço é uma mudança em direção à formalização, um processo trabalhoso para verificar e ampliar o raciocínio matemático. Embora não exijam IA, novas ferramentas automatizadas simplificaram este processo. O assistente de prova de código aberto Lean, desenvolvido na Microsoft Research em 2013, ganhou amplo uso para formalizar provas, e ferramentas de IA como o Aristóteles da Harmonic visam automatizar grande parte desse trabalho. Tudor Achim, fundador da Harmonic, afirmou que o envolvimento de matemáticos e professores de ciência da computação com ferramentas de IA era mais significativo do que o número de problemas de Erdős resolvidos. Achim disse: “Essas pessoas têm reputações a proteger, então, quando dizem que usam Aristóteles ou ChatGPT, isso é uma evidência real”.
