Lean, Coq e Isabelle: como assistentes de prova estão mudando as provas matemáticas

Agora o software entrou no jogo - e encontra falhas que ninguém conseguia enxergar.

Durante muito tempo, em escritórios silenciosos entre quadros de giz e cadernos cheios de anotações, vigorou uma regra não escrita: um resultado é tão confiável quanto os melhores especialistas da área acreditarem que ele é. Só que esse período está perdendo força. Cada vez mais pesquisadores de ponta estão fazendo com que programas como Lean, Coq e Isabelle recalcularem seus teoremas linha por linha. O que antes era obra de gênios isolados passa a virar um trabalho conectado; o que antes era confiança vira lógica verificável em código.

Do gênio solitário ao projeto em rede

Por séculos, a pesquisa em matemática seguiu um roteiro quase fixo: uma pessoa - ou um grupo pequeno - desenvolve a ideia do argumento, escreve um rascunho de prova, envia a uma revista, e então colegas passam meses lendo e checando. Na melhor hipótese, ninguém encontra brechas. Na pior, anos depois alguém percebe um erro que derruba tudo.

Essa sensação de incerteza também apareceu para Peter Scholze, um dos matemáticos alemães mais conhecidos e vencedor da Medalha Fields. Em 2018, ele publicou uma prova extremamente complexa sobre os chamados “espaços compactos”, em uma formulação nova e altamente abstrata. No planeta inteiro, apenas um grupo muito reduzido de pessoas conseguia acompanhar os detalhes. O próprio Scholze não tinha certeza absoluta de que algum deslize minúsculo não tivesse passado despercebido.

Em vez de pedir mais pareceres, ele adotou uma alternativa radical: anunciou publicamente o “Liquid Tensor Experiment”. A proposta era simples e dura: quem dominasse o software de provas Lean deveria tentar formalizar toda a argumentação nessa linguagem. Nada de texto solto - e sim código rigorosamente estruturado, que uma máquina entende e consegue checar.

“Um teorema, nesse novo cenário, só passa a ser aceito quando não apenas pessoas, mas também um algoritmo rigoroso libera cada linha.”

Depois de cerca de seis meses, um time internacional anunciou que tinha dado certo: aproximadamente 180.000 linhas de código em Lean cobriam a argumentação inteira - sem nenhuma lacuna lógica. Para Scholze, isso representava um patamar de qualidade diferente de qualquer avaliação tradicional. Para a comunidade, foi um divisor de águas: um ofício milenar ganhou, de repente, o formato de um empreendimento coletivo com apoio computacional.

Software torna controláveis provas antes “impraticáveis” de verificar

O episódio de Scholze não ficou sozinho. Há outro caso emblemático: a matemática ucraniana Maryna Viazovska resolveu um enigma antigo sobre o empacotamento mais denso de esferas em oito dimensões - um problema muito abstrato que permaneceu em aberto por séculos. A solução rendeu a ela a Medalha Fields em 2022.

A arquitetura da prova era brilhante, mas tão compacta e técnica que uma checagem manual completa consumiria anos. Por isso, um grupo de pesquisadores decidiu traduzir o trabalho para Lean. Durante meses, eles quebraram cada trecho em passos lógicos ainda menores, até que toda a prova existisse como um programa. Em 2024, o código integral foi publicado no GitHub - e o resultado passou a estar garantido também em formato formal e legível por máquina.

Aí está o ponto explosivo dessa tecnologia: argumentos que antes eram considerados “longos demais”, “técnicos demais” ou “na prática impossíveis de conferir” passam a poder ser divididos em partes manejáveis.

• Teoremas gigantes podem ser separados em muitos blocos pequenos.
• Equipes em vários continentes conseguem trabalhar em paralelo em diferentes seções.
• No fim, a máquina conecta todas as peças e verifica a lógica do conjunto.

Um componente central nesse ecossistema é a Mathlib, a grande biblioteca padrão do Lean. Ela já reúne mais de um milhão de linhas com definições formalizadas e teoremas provados. Assim, novas provas podem se apoiar nesse alicerce que não para de crescer, sem precisar recomeçar do zero. O resultado é um ganho enorme de velocidade e uma redução na barreira de entrada.

Quando o computador corrige vencedores da Medalha Fields

Esses programas não servem apenas para confirmar provas que já estão corretas. Eles também expõem fragilidades que até especialistas deixam passar. Em 2021, pesquisadores formalizaram em Lean um resultado já premiado. A pesquisa era respeitada na área, um prêmio havia sido concedido, e a reputação estava estabelecida.

Ao converter o argumento para código, o Lean travou em uma construção intermediária: faltava uma hipótese, e a cadeia lógica não estava fechada de forma precisa. Nenhuma revisão humana tinha notado essa inconsistência antes. Os autores precisaram ajustar o raciocínio e escrever tudo com mais rigor.

Isso deixa claro como esses instrumentos funcionam. Enquanto uma leitora humana, diante de uma prova de 100 páginas, pode se cansar ou acabar “passando por cima” por hábito, o software não aceita atalhos. Toda variável precisa estar definida, e toda inferência tem de ser explicitamente justificada. O efeito é direto: menos abreviações informais e mais lógica robusta, comprovável.

“A máquina não negocia: ela exige completude - ou simplesmente se recusa a liberar o próximo passo.”

Como os proof-assistants mudam o dia a dia da matemática

Durante anos, essas ferramentas foram vistas como brinquedos de informáticos teóricos. Para usá-las, era necessário saber programar, ter muita paciência e uma boa tolerância à frustração. Só que essa realidade está mudando depressa.

Interfaces mais modernas e assistentes com apoio de IA estão removendo boa parte dos obstáculos. Modelos de linguagem sugerem trechos de código Lean quando pesquisadores descrevem uma parte da prova escrita à mão. Ambientes interativos mostram, em tempo real, se um passo é formalmente válido ou se ainda faltam hipóteses. Com isso, doutorandos e doutorandas conseguem aprender gradualmente a converter ideias em código preciso.

O que Lean, Coq e Isabelle realmente fazem

Todas essas ferramentas fazem parte do grupo dos chamados assistentes de prova (proof-assistants). A lógica central é a seguinte:

• Afirmações matemáticas são convertidas para uma linguagem formal estrita.
• O programa opera com um conjunto fixo de regras de lógica e inferências permitidas.
• Cada passo da prova precisa ser justificável dentro dessas regras.
• Se houver um salto ou um buraco em qualquer ponto, o processo de prova é interrompido.

Em vez de “inventar” automaticamente uma prova completa, esses sistemas acompanham a pessoa na construção. Eles sugerem subcaminhos, testam hipóteses e apontam alternativas quando uma tentativa termina em beco sem saída. No melhor cenário, surge um diálogo: a intuição de um lado e a exigência formal do outro.

Oportunidades, riscos e perguntas em aberto

Os ganhos são óbvios: mais segurança de que resultados publicados realmente se sustentam. Verificação mais rápida de projetos extremamente complexos. E maior rastreabilidade, porque cada passo fica explícito no código.

Ao mesmo tempo, aparece uma questão delicada: até que ponto a comunidade pode depender desse software? Será que, em algum momento, pesquisadores vão apenas conferir se o computador “ficou verde”, sem compreender cada etapa? Já há quem alerte para uma espécie de “matemática no piloto automático”, em que só poucos especialistas entendem de verdade o código das próprias ferramentas.

Também existe o problema da dependência de plataformas e linguagens específicas. Quem constrói uma carreira em provas em Lean fica ligado a um ecossistema. E se, um dia, a comunidade migrar para outro sistema? Esse tipo de preocupação tem aparecido cada vez mais nas discussões técnicas.

O que muda para estudantes e docentes

Em muitas universidades, disciplinas de provas formais e assistentes de prova estão entrando no currículo. Além das estratégias clássicas, estudantes aprendem a codificar argumentos de forma formal. Isso aprofunda o entendimento: quando alguém é forçado a explicitar cada frase “óbvia”, fica evidente onde antes havia apenas sensação - e não compreensão real.

Docentes veem nisso uma chance de trazer mais transparência. Questões de prova, por exemplo, podem vir acompanhadas de scripts simples em Lean, permitindo que alunos testem se seus caminhos são logicamente consistentes. Assim, o termo “prova”, muitas vezes tratado como algo quase místico, vira um procedimento bem estruturado, praticável passo a passo.

Como segue: criatividade humana, rigor de máquina

Muitos pesquisadores acreditam que, nos próximos anos, vai se consolidar um modelo de divisão de trabalho: pessoas criam novos conceitos, arriscam conjecturas ousadas e desenham estratégias gerais. Depois vem o detalhamento no assistente de prova, com apoio de IA, que reconhece padrões adequados a partir de milhões de linhas de código já existentes.

Especialmente na fronteira do conhecimento - onde provas ocupam centenas de páginas ou milhares de linhas - essa combinação pode acelerar muito a área. Projetos antes vistos como “arriscados demais” ou “trabalhosos demais” ficam mais viáveis. Com isso, podem surgir teorias cuja complexidade ultrapassa o que uma única mente conseguiria dominar por completo - mas que, ainda assim, serão consideradas seguras, porque cada linha de lógica formal estará verificável.

Isso também muda a noção do que é uma prova. Ela deixa de ser apenas um texto elegante em uma revista e passa a ser um artefato que mistura texto, código e bibliotecas mantidas coletivamente. A imagem antiga do gênio isolado na mesa dá lugar a equipes conectadas, trabalhando junto com software no limite do que é demonstrável em matemática.