Lean, Coq e Isabelle: como softwares 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 e cadernos, valeu uma regra tácita: um teorema era tão confiável quanto a confiança que os melhores da área depositavam no seu argumento. Esse período está balançando. Cada vez mais pesquisadores de ponta pedem que programas como Lean, Coq ou Isabelle refaçam, linha por linha, a lógica dos seus resultados. O que antes dependia de reputação e leitura atenta passa a virar lógica verificável em código; o que era obra de um indivíduo se transforma em esforço conectado.

Do gênio solitário ao projeto em rede

Por séculos, o roteiro da matemática foi quase sempre o mesmo: uma pessoa - ou um grupo pequeno - descobre uma ideia de prova, escreve o raciocínio, envia a uma revista e, então, colegas passam meses lendo e relendo. Se tudo corre bem, não aparece nenhuma brecha. Se dá azar, alguém encontra anos depois um erro que derruba a construção inteira.

Essa sensação de incerteza também atingiu 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”, apresentada numa formulação nova e altamente abstrata. No mundo todo, apenas um punhado de pessoas conseguia acompanhar o texto - e o próprio Scholze não tinha certeza absoluta de que nenhum detalhe minúsculo estivesse fora do lugar.

Em vez de solicitar ainda mais pareceres, ele escolheu um caminho incomum: anunciou publicamente o “Liquid Tensor Experiment”. A proposta era simples e radical ao mesmo tempo: quem dominasse a linguagem da prova em Lean deveria tentar formalizar toda a argumentação. Nada de texto “solto”; a prova teria de virar código estritamente estruturado, legível e verificável por máquina.

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

Cerca de seis meses depois, um time internacional comunicou que tinha conseguido: aproximadamente 180.000 linhas de código em Lean cobriam toda a cadeia de raciocínio - sem lacunas lógicas. Para Scholze, isso representou um nível de garantia diferente de qualquer revisão tradicional. Para a comunidade, foi um marco: um ofício milenar passou, de repente, a parecer um empreendimento coletivo, apoiado por computador.

Software torna verificáveis provas antes tidas como “impossíveis de checar”

O caso de Scholze não ficou isolado. Outro exemplo de grande visibilidade envolve a matemática ucraniana Maryna Viazovska, que resolveu um problema clássico sobre o empacotamento mais denso de esferas em oito dimensões - um desafio altamente abstrato que permaneceu em aberto por séculos. A solução lhe rendeu, em 2022, também a Medalha Fields.

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

O ponto explosivo dessa tecnologia aparece justamente aí: demonstrações que antes eram classificadas como “longas demais”, “técnicas demais” ou “praticamente impossíveis de verificar” podem ser reestruturadas como projetos editáveis, com partes bem definidas.

• Teoremas gigantescos podem ser divididos em muitos blocos pequenos.
• Equipes em vários continentes conseguem trabalhar em paralelo, cada uma numa parte.
• No final, a máquina junta as peças e valida a lógica do conjunto.

Nesse ecossistema, o Mathlib tem um papel central: trata-se da 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 em crescimento, em vez de recomeçar do zero. O efeito é uma aceleração enorme dos projetos e uma barreira de entrada mais baixa.

Quando o computador corrige vencedores da Medalha Fields

Esses sistemas não servem apenas para carimbar provas que já estavam corretas. Eles também expõem fragilidades que passam batido até por especialistas. Em 2021, pesquisadores formalizaram em Lean um resultado já premiado. O trabalho era respeitado, um prêmio havia sido concedido, a reputação estava consolidada.

Ao converter a prova para código, o Lean travou num passo intermediário: faltava uma condição necessária; a cadeia lógica não estava fechada. Nenhum parecer humano tinha apontado essa inconsistência antes. Os autores precisaram ajustar o argumento e escrever de forma mais precisa.

Isso ilustra bem a natureza dessas ferramentas. Enquanto uma leitora humana, diante de uma prova com 100 páginas, pode se cansar ou “passar reto” por hábito, o software não aceita saltos. Toda variável precisa estar definida com clareza, e toda inferência deve ser justificada de modo explícito. O saldo é menos atalhos informais e mais lógica robusta, demonstrável.

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

Como proof assistants estão mudando o dia a dia da matemática

Por muito tempo, esses sistemas foram tratados como brinquedos de gente da informática teórica. Para usá-los, era preciso saber programar, ter paciência e tolerar bastante fricção. Esse quadro está mudando depressa.

Interfaces mais modernas e assistentes apoiados por IA vêm reduzindo boa parte das barreiras. Modelos de linguagem sugerem trechos de código Lean quando o pesquisador descreve um pedaço da prova escrita à mão. Ambientes interativos indicam em tempo real se um passo está formalmente sustentado ou se ainda faltam hipóteses. Com isso, doutorandas e doutorandos conseguem aprender, etapa por etapa, a converter intuição em código preciso.

O que Lean, Coq e Isabelle realmente fazem

Essas ferramentas pertencem à família dos chamados proof assistants (assistentes de prova). O funcionamento básico segue um princípio comum:

• Afirmações matemáticas são traduzidas para uma linguagem formal rigorosa.
• O programa opera com um conjunto fixo de regras de lógica e inferência permitidas.
• Cada etapa do argumento precisa ser verificável à luz dessas regras.
• Se houver um salto ou uma lacuna em qualquer ponto, o processo de prova para.

Em vez de “inventar” sozinho uma prova completa, o software acompanha a construção feita por pessoas. Ele sugere caminhos intermediários, checa hipóteses e aponta alternativas quando uma tentativa encalha. No melhor cenário, surge um diálogo: de um lado, a intuição humana; do outro, a exigência de rigor formal.

Oportunidades, riscos e perguntas em aberto

Os ganhos são evidentes: mais segurança de que resultados publicados realmente se sustentam; verificação mais rápida de projetos extremamente complexos; rastreabilidade superior, já que cada passo fica registrado de forma explícita no código.

Ao mesmo tempo, aparece uma questão delicada: até que ponto a comunidade pode (ou deve) se apoiar nesses programas? Chegará o dia em que pesquisadores apenas verificarão se o computador “ficou verde”, sem entender o conteúdo passo a passo? Há quem alerte para uma espécie de “matemática no piloto automático”, em que só poucos especialistas compreendem a fundo o próprio código e as engrenagens das ferramentas.

Também existe a dependência de plataformas e linguagens específicas. Quem constrói uma carreira em provas em Lean se vincula a um ecossistema. E se, no futuro, a comunidade migrar para outro sistema? Esse tipo de pergunta vem aparecendo com mais frequência nos debates da área.

O que muda para estudantes e docentes

Em muitas universidades, disciplinas de provas formais e proof assistants estão entrando no currículo. Além das estratégias clássicas de demonstração, estudantes aprendem a codificar argumentos de modo formal. Isso aprofunda a compreensão: quando alguém é obrigado a tornar explícita cada afirmação “óbvia”, fica claro onde antes havia apenas sensação de entendimento - e não entendimento de fato.

Docentes veem aí uma oportunidade de aumentar a transparência. Questões de prova, por exemplo, podem vir acompanhadas de scripts simples em Lean, permitindo que o aluno teste se o raciocínio está logicamente consistente. Assim, o termo “prova” perde um pouco do ar místico e vira um processo estruturado, treinável passo a passo.

Para onde vai: criatividade humana, rigor de máquina

Muitos pesquisadores apostam que, nos próximos anos, um modelo de divisão de trabalho deve se consolidar: pessoas criam conceitos novos, fazem conjecturas ousadas e rascunham estratégias gerais. Depois, começa o trabalho minucioso no proof assistant, com apoio de IA, que identifica padrões úteis a partir de milhões de linhas de código já existentes.

Especialmente na fronteira do conhecimento - onde provas têm centenas de páginas ou milhares de linhas de código -, essa combinação pode acelerar a disciplina de forma significativa. Projetos antes vistos como “arriscados demais” ou “trabalhosos demais” ficam mais viáveis. E podem surgir teorias com uma complexidade muito acima do que qualquer mente isolada conseguiria abarcar por completo - mas que, ainda assim, serão consideradas seguras porque cada linha de lógica formal estará verificável.

Com isso, muda também a noção do que é uma prova. Ela deixa de ser apenas um texto elegante numa revista especializada e passa a ser um objeto composto por texto, código e bibliotecas mantidas coletivamente. A imagem do gênio solitário na mesa dá lugar a equipes conectadas que, junto com software, trabalham no limite do que é demonstrável em matemática.