Um brasileiro nos bastidores de uma revolução na matemática

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? No caso de Navier-Stokes, que tem centenas de milhares de linhas em Lean, membros da comunidade checaram a prova com verificadores que eles mesmos construíram, e ela passou.

Então, a crise de confiança está mais no nível ético, em acusações como a de que empresas de IA gastam água demais e roubam dados.

São questões importantes, mas não dá para parar a revolução na matemática.

Como a comunidade matemática está reagindo à ascensão da IA? Tem gente animada, gente com medo de ficar obsoleta, gente que acha que a IA vai destruir a matemática.