Como Lean, Coq e Isabelle estão a transformar as demonstrações matemáticas

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

Durante muito tempo, nos gabinetes silenciosos entre quadros de giz e blocos de notas, vigorou uma regra não escrita: uma demonstração era tão fiável quanto os melhores especialistas da área a considerassem. Essa época está a vacilar. Cada vez mais investigadores de topo mandam verificar os seus teoremas, linha a linha, por programas como Lean, Coq ou Isabelle. Os génios isolados dão lugar a equipas interligadas, e a confiança transforma-se em lógica verificável através de código.

Do génio solitário ao projeto em rede

Durante séculos, a investigação em matemática seguiu a mesma fórmula: uma pessoa, ou um pequeno grupo, desenvolve uma ideia de demonstração, escreve-a, envia-a para revistas científicas e espera que outros colegas a analisem durante meses. Com sorte, ninguém encontra uma lacuna. Com azar, anos mais tarde alguém descobre um erro capaz de derrubar todo o resultado.

Peter Scholze, um dos matemáticos alemães mais conhecidos e vencedor da Medalha Fields, também sentiu essa incerteza. Em 2018, publicou uma demonstração extremamente complexa sobre os chamados “espaços compactos”, apresentada numa formulação nova e altamente abstrata. Só um reduzido grupo de pessoas no mundo conseguia sequer acompanhá-la. O próprio Scholze não tinha a certeza absoluta de que não existisse, algures, um pequeno erro de raciocínio.

Em vez de pedir mais pareceres, optou por uma via radicalmente diferente: lançou publicamente o “Liquid Tensor Experiment”. A proposta era simples: quem dominasse o software de demonstração Lean deveria tentar formalizar toda a sua argumentação nessa linguagem. Já não se tratava de texto flexível, mas de código rigorosamente estruturado, compreensível e verificável por uma máquina.

“Neste novo contexto, um teorema só é considerado aceite quando não apenas os humanos, mas também um algoritmo rigoroso aprovam cada uma das linhas.”

Ao fim de cerca de seis meses, uma equipa internacional anunciou que tinha conseguido: aproximadamente 180.000 linhas de código Lean cobriam toda a argumentação, sem qualquer lacuna lógica. Para Scholze, este era um patamar de qualidade diferente de qualquer revisão tradicional. Para a comunidade, representou um momento decisivo: uma prática com milhares de anos tornou-se, de repente, um empreendimento coletivo apoiado por computadores.

O software torna verificáveis demonstrações aparentemente “impossíveis de conferir”

O caso de Scholze não foi isolado. Outro exemplo conhecido é o da matemática ucraniana Maryna Viazovska, que resolveu um antigo enigma sobre o empacotamento mais denso de esferas em oito dimensões - um problema extremamente abstrato que permanecera em aberto durante séculos. A solução valeu-lhe também a Medalha Fields em 2022.

A estrutura da demonstração era brilhante, mas tão densa que uma verificação manual completa teria exigido anos. Por isso, um grupo de investigadores decidiu traduzi-la para Lean. Durante meses, dividiram cada secção em passos lógicos ainda mais pequenos, até toda a demonstração passar a existir como programa. Em 2024, o código integral foi publicado no GitHub, deixando a demonstração assegurada também numa versão formal e legível por máquinas.

É aqui que reside o verdadeiro potencial desta tecnologia: demonstrações antes classificadas como “demasiado longas”, “demasiado técnicas” ou “praticamente impossíveis de verificar” podem passar a ser divididas em subprojetos geríveis.

• Teoremas de enorme dimensão podem ser repartidos em muitos blocos pequenos.
• Equipas distribuídas por vários continentes conseguem trabalhar em paralelo em partes distintas.
• No final, a máquina reúne todas as peças do puzzle e verifica a lógica do conjunto.

Neste processo, Mathlib, a grande biblioteca-padrão de Lean, tem um papel central. Inclui já mais de um milhão de linhas de definições formalizadas e teoremas demonstrados. Cada nova demonstração pode assentar nessa base em crescimento, em vez de formular tudo desde o início. Isto acelera os projetos de forma significativa e reduz a barreira de entrada.

Quando o computador corrige vencedores da Medalha Fields

Estes programas não servem apenas para confirmar demonstrações que já estão corretas. Também revelam fragilidades que escapam até a especialistas. Em 2021, investigadores formalizaram em Lean um resultado que já tinha recebido um prémio. O trabalho era reconhecido nos círculos científicos, o prémio fora atribuído e a reputação estava estabelecida.

Ao converterem a demonstração em código, Lean bloqueou numa construção intermédia: faltava uma condição, pelo que a cadeia lógica não estava devidamente fechada. Nenhuma revisão humana tinha detetado antes essa inconsistência. Os autores tiveram de ajustar a argumentação e formulá-la com maior precisão.

Isto ilustra a natureza destas novas ferramentas. Enquanto uma leitora humana pode cansar-se ao analisar uma demonstração de 100 páginas, ou deixar passar algo por hábito, o software não aceita saltos. Todas as variáveis precisam de uma definição clara e cada conclusão deve ter uma justificação exata. O resultado são menos atalhos informais e uma lógica mais robusta e comprovável.

“A máquina não negocia: exige totalidade ou simplesmente recusa aprovar o passo seguinte.”

Como os Proof-Assistants estão a mudar o quotidiano da matemática

Durante muito tempo, estes sistemas foram vistos como brinquedos para informáticos teóricos. Quem pretendesse usá-los precisava de conhecimentos de programação, muita paciência e uma certa tolerância à frustração. Essa situação está a mudar rapidamente.

As interfaces modernas e os assistentes apoiados por IA estão a eliminar grande parte dos obstáculos. Os modelos de linguagem sugerem código Lean quando os investigadores descrevem uma parte da sua demonstração manuscrita. Os ambientes interativos indicam em tempo real se um passo se sustenta formalmente ou se ainda faltam hipóteses. Assim, os doutorandos podem aprender, passo a passo, a converter as suas ideias em código preciso.

O que Lean, Coq e Isabelle realmente fazem

Todas estas ferramentas pertencem ao grupo dos chamados assistentes de demonstração. O seu princípio essencial é o seguinte:

• As afirmações matemáticas são convertidas para uma linguagem formal rigorosa.
• O software trabalha com um conjunto fixo de regras lógicas e de inferências permitidas.
• Cada etapa da demonstração tem de poder ser justificada de acordo com essas regras.
• Se houver um salto ou uma lacuna em algum ponto, o processo de demonstração é interrompido.

Em vez de “inventarem” automaticamente uma demonstração completa, os programas acompanham as pessoas na sua construção. Podem propor caminhos parciais, testar hipóteses ou apresentar alternativas quando uma abordagem chega a um beco sem saída. No melhor cenário, surge um diálogo entre a intuição humana, de um lado, e o rigor formal, do outro.

Oportunidades, riscos e questões em aberto

As vantagens são evidentes: maior segurança de que os resultados publicados resistem ao escrutínio, verificação mais rápida de projetos extremamente complexos e melhor possibilidade de acompanhamento, uma vez que cada passo fica explicitamente registado no código.

Ao mesmo tempo, coloca-se uma questão delicada: até que ponto pode a comunidade confiar neste software? Será que os investigadores acabarão por verificar apenas se o computador apresenta uma “luz verde”, sem compreenderem cada passo? Alguns já alertam para uma espécie de “matemática em piloto automático”, na qual apenas poucos especialistas entendem verdadeiramente o código das próprias ferramentas.

Acresce a dependência de plataformas e linguagens de programação específicas. Quem constrói a carreira sobre demonstrações em Lean fica ligado a um ecossistema. O que acontecerá se, um dia, a comunidade passar a preferir outro sistema? Estas questões surgem cada vez mais nos debates especializados.

O que muda para estudantes e docentes

Em muitas universidades, disciplinas sobre demonstrações formais e Proof-Assistants estão a entrar nos planos de estudo. Além das estratégias clássicas de demonstração, os estudantes aprendem a codificar formalmente os seus argumentos. Isto aprofunda a compreensão: quem é obrigado a explicitar cada afirmação aparentemente “óbvia” percebe rapidamente onde antes apenas tinha uma sensação, sem entender realmente o assunto.

Os docentes veem neste processo uma oportunidade para criar mais transparência. Os exercícios de avaliação podem, por exemplo, incluir scripts simples de Lean, permitindo aos alunos testar se as suas abordagens são logicamente suficientemente rigorosas. Desta forma, o conceito muitas vezes misterioso de “demonstração” torna-se um processo claramente estruturado, que pode ser praticado etapa a etapa.

O futuro: criatividade humana, rigor das máquinas

Muitos investigadores assumem que, nos próximos anos, se consolidará um modelo de divisão de trabalho: as pessoas criam novos conceitos, arriscam conjecturas ousadas e esboçam estratégias gerais. Depois começa o trabalho minucioso no Proof-Assistant, apoiado por IA capaz de identificar padrões adequados em milhões de linhas de código existente.

Precisamente na fronteira do conhecimento, onde as demonstrações ocupam várias centenas de páginas ou milhares de linhas de código, esta combinação poderá fazer avançar fortemente a disciplina. Projetos antes considerados “demasiado arriscados” ou “demasiado exigentes” tornam-se mais realistas. Daí poderão nascer teorias cuja complexidade ultrapassa muito aquilo que uma única pessoa conseguiria abarcar por completo - mas que, ainda assim, são consideradas seguras, porque cada linha de lógica formal está disponível para verificação.

Também se altera, assim, a própria ideia do que é uma demonstração. Deixa de ser apenas um texto elegante numa revista científica e passa a ser uma estrutura composta por texto, código e bibliotecas mantidas em conjunto. A imagem antiga do génio solitário à secretária dá lugar a equipas em rede que, juntamente com software, trabalham no limite do que é matematicamente demonstrável.