Rio de Janeiro – Criado em 2013 pelo pesquisador brasileiro Leonardo de Moura na Microsoft Research, o sistema Lean consolida-se como um dos principais instrumentos para verificação formal de teoremas, apontou o diretor-geral do Instituto de Matemática Pura e Aplicada (Impa), Marcelo Viana.
O Lean funciona por meio de interação entre o matemático e o computador. O usuário define o teorema a ser provado e, em seguida, insere comandos curtos – como “simplifique”, “reescreva” ou “aplique”. A cada etapa, o programa exibe as hipóteses em jogo e sinaliza o que ainda precisa ser demonstrado, impedindo lacunas lógicas. Quando todos os passos são justificados, o software confirma a validade da prova.
Para acelerar o processo, o sistema recorre à biblioteca MathLib, repositório que já reúne centenas de milhares de resultados formalmente verificados, espalhados por mais de 2 milhões de linhas de código em Lean.
Apesar do apoio computacional, registrar um teorema relevante na linguagem continua trabalhoso. Ainda assim, especialistas veem na ferramenta um divisor de águas para a disciplina. Entre os entusiastas está o australiano Terence Tao, ganhador da Medalha Fields em 2006, que desenvolveu seu próprio verificador para uso em pesquisas.
Imagem: Internet
Em janeiro de 2024, Tao e o colega Alex Kontorovich propuseram a transcrição, em Lean, do Teorema dos Números Primos – resultado central da teoria dos números. No mês passado, a empresa norte-americana Math, Inc. anunciou ter concluído o desafio com apoio de inteligência artificial. Viana adiantou que abordará detalhes do feito em coluna posterior.
Com informações de Folha de S.Paulo
