Como Lean, Coq e Isabelle estão a mudar as provas matemáticas

Agora o software também entra em cena - e encontra falhas que ninguém conseguia ver.

Em gabinetes silenciosos, entre quadros e cadernos de apontamentos, durante muito tempo vigorou uma regra não escrita: um teorema é tão fiável quanto as melhores mentes da área o considerarem. Essa fase está a tremer. Cada vez mais investigadores de topo mandam revalidar os seus resultados, linha a linha, com programas como Lean, Coq ou Isabelle. Onde antes havia génio solitário, surgem equipas distribuídas; onde existia confiança, passa a haver lógica verificável, expressa em código.

Do génio solitário ao projecto em rede

Durante séculos, a investigação em Matemática repetiu um guião familiar: uma pessoa - ou um grupo pequeno - desenvolve a ideia de prova, escreve-a, envia-a para uma revista e, depois, colegas lêem e relêem durante meses. Com sorte, não encontram brechas. Com azar, anos mais tarde alguém descobre um erro capaz de deitar tudo abaixo.

Essa margem de incerteza foi sentida também por Peter Scholze, um dos matemáticos alemães mais reconhecidos e vencedor da Medalha Fields. Em 2018, publicou uma demonstração muito complexa sobre “espaços compactos”, apresentada numa formulação nova e extremamente abstracta. No planeta, apenas um punhado de pessoas tinha capacidade para a acompanhar até ao fim. O próprio Scholze não tinha a certeza absoluta de que não existisse, algures, um deslize minúsculo de raciocínio.

Em vez de pedir ainda mais pareceres, optou por uma via radicalmente diferente: anunciou publicamente o “Liquid Tensor Experiment”. O objectivo era simples de enunciar e difícil de executar: quem dominasse a linguagem de prova Lean deveria tentar formalizar a argumentação completa. Nada de texto solto e interpretável; apenas código rigorosamente estruturado, legível por uma máquina e susceptível de verificação.

Um teorema, neste novo enquadramento, só passa a ser aceite quando não apenas pessoas, mas também um algoritmo rigoroso aprova cada linha.

Ao fim de cerca de seis meses, uma equipa internacional comunicou sucesso: aproximadamente 180.000 linhas de código em Lean cobriam toda a argumentação - sem falhas lógicas. Para Scholze, isto representou um patamar de qualidade diferente de qualquer revisão tradicional. Para a comunidade, foi um momento charneira: um ofício com milénios tornou-se, de repente, um esforço colectivo apoiado por computador.

O software torna controláveis provas aparentemente “impossíveis de verificar”

O caso de Scholze não ficou isolado. Há outro exemplo muito mediático: a matemática ucraniana Maryna Viazovska resolveu um enigma antigo sobre a empacotagem mais densa de esferas em oito dimensões - um problema altamente abstracto que permaneceu em aberto durante séculos. Essa solução valeu-lhe, em 2022, a Medalha Fields.

A arquitectura da prova era brilhante, mas tão compacta e técnica que uma verificação integral, feita apenas à mão, teria consumido anos. Por isso, um grupo de investigadores decidiu traduzir o trabalho para Lean. Durante meses, foram desdobrando cada secção em passos lógicos ainda mais pequenos, até a demonstração existir, por completo, como um programa. Em 2024, o código integral ficou disponível publicamente no GitHub - e o resultado passou a estar garantido também numa forma formal e legível por máquina.

Aqui está o verdadeiro potencial disruptivo desta tecnologia: provas que antes eram rotuladas como “demasiado longas”, “demasiado técnicas” ou “praticamente impossíveis de verificar” podem, de súbito, ser repartidas em subprojectos manejáveis.

• Teoremas de dimensão extrema podem ser divididos em muitos blocos pequenos.
• Equipas em vários continentes conseguem trabalhar em paralelo em partes diferentes.
• No fim, a máquina junta todas as peças e valida a lógica do conjunto.

Neste ecossistema, a Mathlib - a grande biblioteca-padrão do Lean - é decisiva. Já reúne mais de um milhão de linhas com definições formalizadas e teoremas provados. Assim, cada novo projecto consegue assentar nesse alicerce crescente, em vez de recomeçar do zero. O efeito é duplo: acelera-se o trabalho e baixa-se a barreira de entrada.

Quando o computador corrige vencedores da Medalha Fields

Estas ferramentas não servem apenas para carimbar provas que já estavam correctas. Elas também detectam fragilidades que escapam até a especialistas. Em 2021, investigadores formalizaram em Lean um resultado já premiado. O trabalho era respeitado na área, o prémio estava atribuído, a reputação era sólida.

Ao converterem a demonstração para código, o Lean bloqueou num passo intermédio: faltava uma condição necessária e a cadeia lógica não estava devidamente fechada. Nenhuma revisão humana tinha assinalado aquela inconsistência antes. Os autores tiveram de ajustar a argumentação e torná-la mais precisa.

Isto expõe bem a natureza destas ferramentas. Uma leitora humana, diante de uma prova com 100 páginas, acaba por se cansar ou por “passar por cima” de certos pontos por hábito. Já o software não tolera saltos. Cada variável exige uma definição explícita; cada inferência tem de estar fundamentada com exactidão. O resultado é menos atalhos informais e mais lógica robusta, comprovável.

A máquina não negocia: exige completude - ou simplesmente recusa autorizar o passo seguinte.

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

Durante muito tempo, estes sistemas foram vistos como brinquedos de informáticos teóricos. Para os usar, era preciso saber programar, ter muita paciência e uma boa dose de resistência à frustração. Esse cenário está a mudar depressa.

Interfaces mais modernas e assistentes apoiados por IA estão a eliminar boa parte das dificuldades. Modelos de linguagem sugerem código Lean quando uma investigadora descreve uma parte da prova manuscrita. Ambientes interactivos indicam, em tempo real, se um passo é formalmente válido ou se ainda faltam hipóteses. Para doutorandos, isto cria uma aprendizagem guiada: transformar ideias em código preciso, etapa a etapa.

O que o Lean, o Coq e o Isabelle realmente fazem

Todas estas ferramentas pertencem à família dos chamados assistentes de prova. O princípio base é o seguinte:

• As afirmações matemáticas são convertidas para uma linguagem formal estrita.
• O software dispõe de um conjunto fixo de regras lógicas e de inferências permitidas.
• Cada passo da prova tem de ser justificável segundo essas regras.
• Se existir um salto ou uma lacuna em qualquer ponto, o processo de prova interrompe-se.

Em vez de “inventarem” automaticamente uma demonstração completa, estes programas acompanham a construção feita por pessoas. Podem sugerir caminhos intermédios, testar hipóteses, ou apontar alternativas quando uma abordagem encalha. No melhor dos casos, forma-se um diálogo: intuição de um lado, rigor formal do outro.

Oportunidades, riscos e questões em aberto

As vantagens são evidentes: maior confiança de que os resultados publicados se sustentam. Verificação mais rápida de projectos extremamente complexos. Melhor rastreabilidade, porque cada passo fica explícito no código.

Ao mesmo tempo, surge uma pergunta sensível: até que ponto a comunidade pode depender deste tipo de software? Chegará um dia em que os investigadores apenas confirmam que o computador ficou “a verde”, sem compreenderem os passos? Há quem alerte para uma espécie de “Matemática em piloto automático”, em que só um grupo restrito percebe realmente o código e, sobretudo, as próprias ferramentas.

Acresce ainda a dependência de plataformas e linguagens específicas. Quem constrói uma carreira baseada em provas em Lean prende-se, na prática, a um ecossistema. O que acontece se, um dia, a comunidade migrar para outro sistema? Este tipo de questão aparece cada vez mais em debates especializados.

O que muda para estudantes e docentes

Em muitas universidades, disciplinas sobre provas formais e assistentes de prova estão a entrar no currículo. Além das estratégias clássicas, os estudantes aprendem a codificar argumentos de forma rigorosa. Isso afina o entendimento: quando se é obrigado a explicitar cada afirmação supostamente “óbvia”, percebe-se rapidamente onde antes havia apenas intuição, e não compreensão real.

Para docentes, isto também é visto como uma oportunidade de aumentar a transparência. Por exemplo, exercícios de avaliação podem vir acompanhados de pequenos scripts em Lean, permitindo que os alunos testem se a linha de raciocínio está logicamente bem fechada. Assim, o termo “prova”, muitas vezes envolto em mistério, transforma-se num processo claro, estruturado e praticável passo a passo.

Como isto evolui: criatividade humana, rigor da máquina

Muitos investigadores acreditam que, nos próximos anos, se vai firmar um modelo de trabalho por especialização: pessoas introduzem conceitos novos, arriscam conjecturas ousadas e esboçam estratégias gerais. Depois, começa o trabalho minucioso no proof-assistant, apoiado por IA que reconhece padrões úteis a partir de milhões de linhas de código existentes.

Sobretudo na fronteira do conhecimento - onde provas chegam a várias centenas de páginas ou a milhares de linhas de código - esta combinação pode acelerar a disciplina de forma significativa. Projectos antes considerados “demasiado arriscados” ou “demasiado trabalhosos” tornam-se mais viáveis. Podem emergir teorias de complexidade muito acima daquilo que uma única pessoa conseguiria abarcar por completo - e, ainda assim, serem aceites como seguras, porque cada linha de lógica formal fica verificável.

Com isso, também muda a própria noção de prova. Deixa de ser apenas um texto elegante numa revista científica, para passar a ser um objecto feito de texto, código e bibliotecas mantidas em conjunto. A imagem antiga do génio sozinho à secretária dá lugar a equipas em rede que, com a ajuda de software, trabalham no limite do que é demonstrável em Matemática.