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.
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”.
https://super.abril.com.br/tecnologia/um-brasileiro-nos-bastidores-de-uma-revolucao-na-matematica/
ACERCA DEL CORRESPONSAL
REDACCIóN CENTRAL
Prensa Mercosur es un diario online de iniciativa privada que fue fundado en 2001, donde nuestro principal objetivos es trabajar y apoyar a órganos públicos y privados.
