Matemáticos identificam erro na tradução de prova matemática gerada por IA. Um grupo de matemáticos da Universidade de Cambridge questiona a confiabilidade das provas matemáticas geradas por inteligência artificial, após identificar um erro na tradução de uma prova do problema de Navier-Stokes.

A OpenAI anunciou recentemente ter encontrado uma solução para o famoso problema de Navier-Stokes, um dos maiores desafios matemáticos do mundo. A empresa publicou a prova em duas versões: uma em linguagem natural e outra em código de computador chamado Lean.

No entanto, um grupo liderado por Anders Hansen, da Universidade de Cambridge, apontou que as duas versões da prova não correspondem exatamente. O erro está na tradução do Lean, que foi feita automaticamente pela IA, resultando em uma versão matematicamente mais fraca.

Segundo Hansen, este erro indica que a tradução automática pode não ser totalmente precisa, levantando dúvidas sobre a confiabilidade das provas geradas por IA. 'O processo de formalização está tentando substituir a revisão por pares', explica Hansen, 'mas mostramos que este tipo de auto-formalização não pode servir o mesmo propósito'.