Em entrevistas publicadas em 19 de outubro, os matemáticos da Universidade da Califórnia em Berkeley Richard Borcherds e Robin Huang divergiram sobre o papel da IA na matemática. Uma análise publicada em 6 de outubro apontou diferenças entre trechos da prova de Navier–Stokes da OpenAI e sua formalização em Lean, mas seus autores não afirmaram que a prova em linguagem natural esteja errada.
O que os matemáticos de Berkeley disseram sobre IA
O The Daily Californian relatou que Borcherds vê a IA como uma força capaz de superar matemáticos humanos em certas tarefas e de mudar a pesquisa em pouco tempo. Huang mostrou-se menos convencida das capacidades atuais da tecnologia e manifestou preocupação com seus efeitos na comunidade matemática. São avaliações pessoais distintas, não uma posição comum dos pesquisadores.
O resultado que a OpenAI afirma ter obtido
Em 8 de setembro, a OpenAI anunciou uma prova para o problema de existência e suavidade de Navier–Stokes. A empresa afirma que um fluido incompressível em três dimensões, inicialmente em repouso e sujeito a uma força externa suave, pode desenvolver uma singularidade em tempo finito, enquanto sua energia permanece finita. A OpenAI diz que o resultado trata das afirmações C e D da formulação do problema do Instituto de Matemática Clay.
A empresa também informou que o grupo de agentes responsável pelo resultado tinha cerca de 10 mil agentes simultâneos. Segundo a OpenAI, eles chegaram ao resultado em aproximadamente 88 horas; a formalização e a verificação em Lean levaram mais 17 horas.
Em outubro, a NeoTeo também abordou a divulgação de outros resultados matemáticos gerados por um modelo interno da OpenAI. O caso de Navier–Stokes envolve uma afirmação matemática específica, acompanhada de uma prova em texto e de uma formalização.
A diferença apontada entre o texto e Lean
Lean é uma linguagem formal e um assistente de provas: ele permite codificar uma afirmação matemática e verificar se os passos escritos no código demonstram essa afirmação. A questão levantada por A. Bastounis, F. Circelli e A. C. Hansen é se a formalização codifica fielmente o que a prova em linguagem natural afirma e argumenta.
Em um artigo publicado em 6 de outubro, os autores comparam a estimativa da equação 8.19 do texto da OpenAI com uma estimativa citada na formalização em Lean. No texto, o limite para a função de entrada F envolve quatro derivadas adicionais; na estimativa em Lean, envolve cinco.
| Versão da estimativa | Derivadas adicionais exigidas para F |
| Texto em linguagem natural | 4 |
| Estimativa citada em Lean | 5 |
A diferença torna a estimativa em Lean mais fraca nesse ponto: ela exige uma derivada adicional para controlar as mesmas derivadas do resultado. Os autores também comparam a estimativa do fluxo de pressão. No texto, ela depende de B_R; na versão em Lean, depende também de A_R, e os autores consideram difícil comparar diretamente os dois limites.
O que a verificação em Lean pode dizer
Quando uma prova compila em Lean, isso verifica a demonstração da afirmação que foi codificada. Essa checagem, por si só, não mostra que a afirmação e o raciocínio codificados preservam o sentido do texto original. Essa distinção é o foco da análise de Bastounis, Circelli e Hansen. Os autores delimitam sua conclusão às diferenças entre a prova escrita e a formalização que examinaram e não afirmam que a prova em linguagem natural da OpenAI esteja incorreta.
A OpenAI publicou sua descrição do resultado e da formalização em Lean em seu anúncio sobre o problema de Navier–Stokes.
