Brasileiro cria linguagem que revoluciona verificação de provas na matemática

Criado em 2013 pelo cientista carioca Leonardo de Moura, o Lean é uma linguagem de programação voltada para verificar provas matemáticas em busca de lacunas e deslizes, garantindo rigor lógico absoluto. O sistema ganhou forte repercussão global e passou a ser adotado até por medalhistas Fields para checar conjecturas complexas.

Em setembro, a ferramenta esteve no centro de discussões quando a OpenAI anunciou uma solução para o problema matemático de Navier-Stokes, um dos sete Problemas do Milênio, avaliados em US$ 1 milhão cada. O código com centenas de milhares de linhas em Lean passou pelos verificadores da comunidade, confirmando a impecabilidade lógica da prova, ainda que o debate ético sobre inteligência artificial permaneça em pauta entre especialistas.

Em entrevista, Leonardo de Moura relembrou que a utilidade atual do Lean junto à inteligência artificial não era imaginada nem mesmo em 2023. Originalmente, o sistema era utilizado na Microsoft para testar a ausência de bugs em softwares, aplicando-se apenas a áreas altamente críticas devido ao alto custo computacional e de desenvolvimento.

A ascensão da inteligência artificial na área gera reações diversas na comunidade acadêmica, dividindo opiniões entre entusiasmo, receio de obsolescência e ceticismo. Enquanto grandes nomes da matemática debatem os limites da tecnologia, projetos de formalização que levariam anos foram concluídos em questão de dias com o suporte de ferramentas automatizadas.

Com informações de: Super Interessante