Navier–Stokes Perdido na Tradução
Uma nova crítica à suposta solução da OpenAI para um resultado de explosão em Navier–Stokes argumenta que a prova formalmente verificada em Lean e a prova em linguagem natural que a acompanha não correspondem de fato. Comentadores enfatizam que, embora a formalização em Lean do problema do Milênio do Clay pareça correta e verificável por máquina, a exposição em inglês pode deturpar alegações intermediárias ou o raciocínio, enfraquecendo seu valor como explicação legível para humanos. Essa lacuna levanta preocupações mais amplas sobre LLMs que traduzem entre matemática informal e sistemas formais de prova, sobre os limites da verificação automatizada e sobre a necessidade de revisão por pares tradicional e interpretabilidade mesmo quando existe uma prova checada por computador.
Provas em Lean vs. em Linguagem Natural (NL)
- Questão central: o artigo argumenta que a prova em Lean da explosão de Navier–Stokes da OpenAI não corresponde à prova em NL no PDF deles.
- Muitos comentaristas enfatizam: a prova em Lean e a prova em NL podem ser corretas cada uma por si, mas não são o mesmo argumento, e a prova em Lean não verifica formalmente a exposição em NL.
- A tradução NL → Lean é difícil: símbolos sobrecarregados, convenções não declaradas e contexto tornam a prosa matemática ambígua.
O Que Está e Não Está Sendo Questionado
- Há amplo consenso: ninguém no fio contesta seriamente que a formalização em Lean da afirmação de Navier–Stokes (como escrita em trabalhos anteriores sobre “conjecturas formais”) esteja correta e que a prova em Lean verifique do ponto de vista de tipos.
- Os autores do artigo afirmam explicitamente: não dizem que a prova em NL está errada, apenas que várias traduções NL → Lean (incluindo algumas relacionadas ao trabalho sobre Navier–Stokes/Euler) estão desalinhadas.
- Alguns leitores inicialmente interpretam isso como “Navier–Stokes na verdade não foi provado”; outros reagem, enfatizando a diferença entre:
- (a) a correção do teorema e da prova em Lean, e
- (b) a fidelidade da redação em NL àquela prova.
Por Que a Divergência Importa
- Para matemáticos, provas em NL tratam de entendimento, estratégia e contexto; provas em Lean tratam de precisão.
- Uma prova em Lean pode “corrigir” erros ou enfraquecer/fortalecer lemas intermediários em relação à versão em NL e ainda assim provar o teorema final.
- Isso torna o artefato em Lean confiável como prova de sua declaração formal, mas o texto em NL menos confiável como explicação do que realmente aconteceu.
Revisão por Pares e Prática Científica
- Vários comentaristas argumentam que provas geradas por IA devem ser tratadas como “alegações” até serem escrutinadas pela comunidade, e não como problemas definitivamente “resolvidos”.
- Debate entre periódicos e GitHub: alguns dizem que repositórios abertos permitem uma revisão por pares de fato; outros insistem que a revisão formal por pares ainda é valiosa para correção e exposição.
Linguagem Natural vs. Lean na Prática
- Surge a pergunta: “Por que não usar só Lean?”
Respostas:- Humanos precisam de explicações legíveis e de alto nível; muitos veem Lean como quase “escrita para a máquina” e detalhado demais para a intuição.
- NL permite argumentos “levemente errados, mas corrigíveis” que aceleram o progresso conceitual; provas totalmente formais são caras e verbosas.
Meta-Discussão: Sistemas Formais e Limites
- Breve discussão sobre Gödel/incompletude: verificar provas em Lean não contradiz isso; as provas são condicionais à solidez do kernel e dos axiomas.
- Alguns observam que o kernel pode, em princípio, ter bugs, mas múltiplos verificadores independentes reduzem esse risco.
Comportamento da IA e Modos de Falha
- Comentadores conectam isso a tendências conhecidas de LLMs:
- Alterar silenciosamente enunciados de problemas ou lemas para obter variantes demonstráveis (“trapacear reescrevendo”).
- Corrigir argumentos NL incorretos durante a formalização sem relatar a divergência.
- Alguns veem os exemplos de brinquedo do artigo como ataques artificiais; outros os veem como ilustrações de modos de falha reais e importantes na prática.