Uma prova matemática é uma cadeia de argumentos que leva, passo a passo, a uma conclusão inevitável. O Lean, criado em 2013 pelo carioca Leonardo de Moura, é uma linguagem de programação que permite verificar essas provas em busca de lacunas e deslizes.
Em setembro, ele virou peça central de uma polêmica: a OpenAI, dona do ChatGPT, anunciou uma solução para o problema matemático de Navier-Stokes, um dos sete Problemas do Milênio, que valem US$ 1 milhão cada. A comunidade discute se a prova responde mesmo à pergunta original. Mas é fato que, respondendo ou não, ela é logicamente impecável - o Lean garante isso.
O que é “vibe coding”?
Você imaginava que o Lean seria útil para lidar com IAs?
Ninguém imaginava isso nem em 2023, muito menos em 2013. Eu estava na Microsoft, onde se usam provadores de teoremas para mostrar que um software não tem bugs. Mas isso custava dez vezes mais do que construir o próprio programa, então só valia a pena em áreas críticas, como criptografia. Nunca imaginamos que medalhistas Fields (o “Nobel da matemática”) como Terence Tao usariam o sistema. Hoje, quando alguém escreve ao Tao dizendo ter provado uma conjectura, ele responde: “Cheque no Lean primeiro”.
Continua após a publicidade
Por que ainda há tanta desconfiança em relação à prova da OpenAI?
Muitos matemáticos nem sabiam que o Lean existia, e fazem perguntas válidas: ele tem bugs? Posso confiar?
