OpenAI diz que modelo de IA gerou prova formal em Lean para suposto colapso das equações de Navier–Stokes
Empresa afirma que execução com ~10.000 agentes custou milhões; resultado ainda precisa de documentação pública, revisão por pares e verificação independente
A OpenAI anunciou nesta terça que um modelo interno não divulgado produziu uma prova formalizada em Lean que afirma a existência de uma singularidade em tempo finito para as equações de Navier–Stokes em três dimensões.
Segundo a empresa, o resultado veio de uma execução multiagente com cerca de 10.000 agentes concorrentes ao longo de aproximadamente 88 horas, e o esforço custou milhões de dólares (US$).
O matemático da NYU Tristan Buckmaster e o pesquisador da Anthropic Levent Alpöge publicaram avanços relacionados anteriormente; a OpenAI diz que intensificou o trabalho depois de saber do progresso deles e questionou arranjos de autoria propostos.
A OpenAI nega ter inspecionado os rascunhos de Buckmaster e Alpöge, mas admite que não pode descartar que dados de usuários desidentificados tenham ajudado a melhorar os modelos. A empresa também afirma que não buscará o prêmio do Clay Mathematics Institute.
A comunidade matemática mais ampla ainda não aceitou a alegação. Para o problema de Navier–Stokes ser dado como resolvido será necessário que a prova tenha documentação pública, passe por revisão por pares e seja verificada de forma independente.