OpenAI divulga prova alegada do problema de Navier–Stokes e arquivos formais verificáveis
Publicação levanta dúvidas sobre créditos, uso de dados de treinamento e rapidez com que empresas de IA devem anunciar resultados matemáticos
OpenAI disse que um modelo interno não divulgado, usando cerca de 10.000 agentes cooperantes, gerou uma proposta de solução para o problema da existência e suavidade das equações de Navier–Stokes após aproximadamente 88 horas de busca e cerca de 17 horas de formalização em Lean.
A empresa publicou um artigo de 166 páginas e os arquivos da prova em Lean, mas afirmou que não vai concorrer ao Prêmio do Milênio da Clay Mathematics Institute e ressaltou que ainda é necessária verificação humana.
O matemático da NYU Tristan Buckmaster acusou publicamente a OpenAI de seguir uma abordagem parecida com trabalho inédito que ele fez com Levent Alpöge e questionou se o uso das ferramentas da OpenAI expôs seus rascunhos; a empresa nega acesso direto a materiais não públicos, mas reconheceu que “não pode descartar” a possibilidade de que dados derivados de uso desidentificado tenham influenciado seus modelos.
Vinte e cinco ganhadores da Medalha Fields publicaram uma declaração conjunta alertando que incentivos comerciais para anunciar resultados de impacto rapidamente entram em conflito com as normas da matemática sobre verificação e atribuição cuidadosas. Em meio às críticas, a OpenAI retirou o patrocínio de um evento de matemática do Caltech.
Revisões por pares independentes e escrutínio de especialistas estão em curso para decidir se a formalização em Lean e o argumento sobre uma singularidade em tempo finito se mantêm. Os processos estabelecidos da Clay Mathematics Institute para o Prêmio do Milênio permanecem válidos.
