Lean, o novo tira-teima da matemática

Lean é uma linguagem de programação e verificador de teoremas, criado na Microsoft Research em 2013, com colaboração direta entre matemático e máquina.
O formalismo permite decompor provas em passos simples, até confirmar a veracidade do teorema de forma automática.
A MathLlib (biblioteca de Lean) já reúne centenas de milhares de teoremas, em mais de 2 milhões de linhas de código.
O brasileiro Leonardo de Moura foi um dos criadores e destaque, defendendo o uso colaborativo entre humano e máquina.
Em janeiro de 2024, Terence Tao e Alex Kontorovich desafiaram transcrever para Lean o Teorema dos Números Primos; no mês passado, a empresa Math, Inc. afirmou ter vencido esse desafio com auxílio de inteligência artificial.

Lean, novo tira-teima da matemática

Um novo recurso interativo aproxima matemáticos e máquinas na verificação de teoremas. Criada por brasileiro, a ferramenta facilita a colaboração entre humano e software para validar provas.

A iniciativa tem como foco a redução de lacunas causadas pela complexidade de demonstrações cada vez maiores. Ela utiliza uma biblioteca de teoremas já verificados para apoiar novas provas.

O sistema Lean funciona como uma linguagem de programação e verificador de teoremas desenvolvido na Microsoft Research. O pesquisador formula o teorema e envia comandos simples para que o software confirme cada etapa.

Ao longo do processo, o Lean identifica suposições, sinaliza lacunas lógicas e, ao fim, declara a veracidade da prova. A abordagem evita refazer os passos a cada passo, conectando-os a fundamentos já validados.

A biblioteca MathlLib agrega centenas de milhares de teoremas, contidos em mais de 2 milhões de linhas de código Lean. Essas formalizações ajudam a justificar proposições novas com maior confiabilidade.

Especialistas veem grande potencial no uso dessa metodologia. Entre eles, Terence Tao, ganhador da medalha Fields, que já desenvolveu uma ferramenta própria para apoiar sua pesquisa.

No começo de 2024, Tao e Alex Kontorovich lançaram o desafio de transcrever para Lean o Teorema dos Números Primos. Em janeiro de 2025, a Math, Inc. afirmou ter vencido parcialmente esse desafio com auxílio de inteligência artificial.