A divulgação da solução de Navier-Stokes pela OpenAI incluiu uma prova formal em Lean 4
A alegada solução da OpenAI para um problema do Prêmio Millennium de Navier–Stokes usando “enxames de agentes” de um modelo de linguagem grande e uma prova formal em Lean 4 está provocando tanto admiração quanto ceticismo. Os comentaristas avaliam o feito técnico e a promessa da formalização automática de provas contra custos massivos de computação, dúvidas sobre se a IA plagiou ou dependeu demais do trabalho de pesquisadores humanos e o risco de a matemática virar algo que máquinas fazem sem melhorar a compreensão humana. Muitos também discutem quanta confiança depositar em ferramentas de verificação formal como o Lean, quais bugs ou especificações erradas ainda poderiam invalidar resultados e se tais provas de existência negativas têm aplicações físicas reais.
Custo e Eficiência da Formalização por IA vs Humanos
- O thread contesta a afirmação de economia de “quatro ordens de magnitude”: estimativas de improviso sugerem cerca de ~$40M em computação vs ~$130M em trabalho humano, ainda enorme, mas com uma diferença menor.
- Alguns argumentam que a clássica regra de “40 horas por página” para formalização está desatualizada devido à melhor automação e às bibliotecas; outros a defendem para material complexo de nível de pesquisa.
- Coordenar ~1M de horas de esforço humano é visto como praticamente impossível em comparação com um grande enxame de agentes.
Lean, Autoformalização e Desempenho
- Muitos observam que o Lean moderno + mathlib reduzem dramaticamente o esforço para material de nível de graduação, mas provas de pesquisa profundas ainda exigem trabalho enorme.
- O Lean é considerado lento nessa escala (por exemplo, verificação de vários dias, 230 GB), embora vários apontem que a geração por agentes ocorreu massivamente em paralelo, enquanto a verificação provavelmente foi feita em grande parte em uma única máquina.
- Há discussão sobre otimizar o kernel do Lean e provar versões otimizadas equivalentes à versão simples; projetos que reimplementam o Lean em Lean são mencionados como um caminho.
Verificação, Confiança e Possíveis Bugs
- Consenso: se os axiomas e os enunciados dos teoremas estiverem corretos, uma prova em Lean verificada é altamente confiável; o principal risco é formalizar incorretamente o enunciado, não os passos internos da prova.
- Alguns observam que o Lean já teve bugs no kernel no passado; uma IA poderia, em princípio, explorar um bug desses em vez de realmente provar o teorema.
- Há preocupação com formalizações “adversariais” que alteram sutilmente definições; checar o enunciado do teorema e as hipóteses continua sendo responsabilidade humana.
Ética, Plágio e Uso de Dados
- Grande subthread sobre se as ideias-chave da IA foram “plagiadas” de pesquisadores que usaram modelos anteriores, especialmente via treinamento em chats privados.
- De um lado: cronologia e variantes do problema sugerem que a IA resolveu casos mais difíceis e que o trabalho privado recente não poderia ter estado no run de treinamento.
- Do outro lado: anonimização e mistura de dados de usuários tornam “impossível saber” o que influenciou o modelo; a desconfiança na ética do laboratório amplia a suspeita.
Significado, Compreensão e Valor
- Alguns ficam impressionados com o fato de um modelo geral conseguir tanto resolver quanto verificar formalmente um problema desse tipo; outros temem que o resultado seja “um bit de informação” com pouca compreensão humana associada.
- Crítica de que grandes laboratórios de IA buscam manchetes, não exposição matemática profunda, e que não respondem a perguntas de acompanhamento nem se integram à comunidade matemática mais ampla.
Impacto Prático do Resultado sobre Navier–Stokes
- Debate sobre a relevância no mundo real: alguns acham que esse resultado negativo mostra principalmente que Navier–Stokes é um modelo físico imperfeito; outros veem aplicações imediatas limitadas.
- Comparação com exemplos paradoxais ou altamente artificiais em matemática pura; ceticismo de que tais singularidades importem para engenharia ou modelagem de turbulência.
Reflexões Mais Amplas sobre IA e Matemática
- Emoções mistas: entusiasmo com autoformalização e trabalho futuro em problemas como a conjectura abc, mas também ansiedade de que a criatividade matemática humana esteja sendo “mecanizada”.
- Preocupações com futuras provas geradas por IA que humanos não consigam verificar de forma viável sem enorme computação, e com possíveis ataques às cadeias de ferramentas de verificação formal.