Como os Assistentes de Prova e o Lean estão a mudar a Matemática

De repente, os assistentes de software estão a entrar na disciplina mais “sagrada” da matemática.

O que antes era trabalho solitário e silencioso em gabinetes isolados está a transformar-se, de forma inesperada, num esforço colectivo à escala mundial entre investigadores de topo e computadores. Programas especializados percorrem provas matemáticas linha a linha, detectam falhas onde as pessoas acabariam por desistir e tornam abordáveis problemas que, até há pouco, eram considerados praticamente impossíveis de verificar.

Como os computadores entram na zona sagrada da matemática

Desde os tempos de Arquimedes, o ofício da matemática funcionou, no essencial, da mesma maneira: alguém tem uma ideia, escreve uma prova, envia-a a colegas da área, e esses colegas passam meses a escrutinar páginas e páginas de símbolos, tentando não deixar escapar nenhum erro de raciocínio. Este ritual foi, durante séculos, o padrão-ouro - lento, penoso, mas sem alternativa real.

É precisamente aqui que entra a nova vaga dos chamados “Proof Assistants”, isto é, software que valida cada passo lógico de uma prova. Entre as ferramentas mais conhecidas estão Lean, Coq e Isabelle. Operam como um revisor implacavelmente minucioso: não há saltos, atalhos nem “isto é óbvio” que fiquem por confirmar.

O núcleo da revolução: o computador só aceita aquilo que pode ser decomposto, sem falhas, em lógica rigorosa - sem confiança, sem intuição.

Para isso, os matemáticos têm de verter a prova para uma linguagem formal que o programa consiga interpretar. No fim, o resultado é código onde cada transição fica explicitamente registada. Essa exigência radical corta pela raiz lapsos típicos do trabalho humano: argumentos omitidos, pressupostos não declarados ou pequenos erros de cálculo que acabam por ser fatais.

Caso Scholze: quando até um superstar prefere mandar verificar

Um dos momentos decisivos desta mudança teve origem na Alemanha. O matemático de Bona Peter Scholze, laureado com a Medalha Fields, publicou um teorema extremamente complexo sobre os chamados espaços condensados. A prova ocupava centenas de páginas e era tão abstracta que, na prática, apenas um grupo minúsculo de especialistas tinha capacidade para a ler.

O próprio Scholze não se sentiu totalmente descansado. O receio era simples: numa cadeia de argumentação tão extensa podia esconder-se uma falha pequena, mas decisiva. Em vez de pedir a mais revisores anos de trabalho manual, lançou no final de 2020 uma experiência: o “Liquid Tensor Experiment”.

A proposta era directa: quem dominasse Lean deveria traduzir partes da prova para essa linguagem formal. Matemáticos e informáticos de vários países juntaram-se, dividiram tarefas e deixaram o Lean testar cada bloco. No final, existia um enorme corpo de código com cerca de 180.000 linhas.

Passados seis meses, a equipa anunciou que o objectivo tinha sido cumprido: a máquina aceitou a prova completa. Não apareceu qualquer lacuna lógica, nem contradições. Para Scholze, isto significou um nível de certeza que nenhuma revisão humana, por mais cuidadosa, conseguiria oferecer. E para a comunidade ficou claro que uma tradição com milhares de anos estava a começar a inclinar.

Do lobo solitário ao estaleiro global

Projectos deste tipo também mudam a forma de trabalhar. Onde antes um pequeno número de especialistas lapidava um resultado, hoje dezenas de investigadores repartem a prova em muitos subproblemas. Cada pessoa formaliza a sua parte, e o software encaixa tudo num edifício coerente.

Ferramentas como Lean tornam possível uma espécie de controlo em tempo real: enquanto alguém escreve um lema, o sistema indica de imediato se o raciocínio se sustenta. Os erros deixam de surgir apenas meses depois, num parecer; aparecem logo no momento em que se está a escrever.

• Investigadores em todo o mundo trabalham em paralelo no mesmo teorema.
• Cada passo é validado de forma imediata pelo software.
• Contributos podem ser reutilizados como peças modulares.
• Jovens cientistas conseguem entrar cedo em projectos de grande escala.

Uma actividade frequentemente solitária passa, assim, a parecer-se com um projecto de open-source para provas matemáticas.

Como o software torna possíveis projectos “impossíveis”

Há outro exemplo muito falado: o trabalho da matemática Maryna Viazovska. Ela resolveu um problema antigo sobre a arrumação mais densa de esferas em espaço de oito dimensões e, mais tarde, em 24 dimensões - uma versão de alta dimensão da pergunta sobre como empilhar laranjas da forma mais eficiente. Esta solução valeu-lhe a Medalha Fields em 2022.

O problema estava na verificação: a prova é tão compacta e técnica que, para muitos especialistas, uma revisão manual completa parecia um pesadelo. Por isso, um grupo internacional decidiu formalizar a prova inteira em Lean. O esforço durou meses e o código final foi publicado online em 2024.

O resultado é uma confirmação formal sem margem para interpretações: qualquer imprecisão teria sido imediatamente bloqueada pelo Lean. Iniciativas assim ilustram bem a deslocação em curso na matemática:

Provas que antes eram consideradas “demasiado longas” ou “demasiado opacas” tornam-se, com a automatização, verificáveis - não apesar da sua complexidade, mas precisamente por causa dela.

Uma peça central deste puzzle é a Mathlib, a grande biblioteca padrão do Lean. Neste momento, já contém mais de 1,2 milhões de linhas de matemática formalizada: definições, teoremas e resultados auxiliares demonstrados. Quem inicia um novo projecto consegue apoiar-se nesse material, sem ter de reescrever e recodificar tudo desde o princípio.

Do conjunto de ferramentas à infra-estrutura

Esta biblioteca funciona como um amplificador a longo prazo:

• Cada projecto aumenta o fundo comum.
• Novas provas podem reutilizar directamente blocos anteriores.
• Argumentos padrão mantêm-se consistentes e verificáveis.
• Erros nos alicerces afectariam de imediato grandes áreas - e, por isso, seriam detectados rapidamente.

Assim, vai-se formando uma infra-estrutura robusta, comparável a frameworks de software consolidados em TI. A diferença é que aqui não se trata de aplicações web, mas sim das fundações da matemática pura.

Quando a máquina corrige provas premiadas

Os “Proof Assistants” não servem apenas para carimbar resultados; também actuam como um corrector sem piedade. Num caso de 2021, uma equipa pegou num teorema já premiado e tentou formalizá-lo em Lean. A meio do processo, o sistema travou: uma afirmação intermédia essencial não se deixava provar exactamente como estava escrita.

Os investigadores tiveram de ajustar, tornar um passo mais preciso e corrigir a argumentação. Revisores humanos tinham deixado passar o problema. Não por má-fé, mas por limitação humana: a partir de certo nível de abstracção, ninguém consegue manter na cabeça todas as implicações.

O computador, pelo contrário, não conhece cansaço, não cai na rotina e não se intimida com nomes sonantes. Ou a lógica fecha - ou não fecha.

Novas barreiras de entrada, novas ajudas

Durante muito tempo, estas ferramentas foram vistas, mesmo entre matemáticos, como brinquedos de nicho para informáticos. A aprendizagem era dura e a sintaxe pouco familiar. Isso está a mudar rapidamente. Interfaces mais confortáveis e módulos de IA integrados estão a guiar os utilizadores.

Modelos de linguagem conseguem converter esboços manuscritos ou formulações em LaTeX para código formal em Lean, sugerem teoremas adequados a partir da Mathlib e preenchem passagens rotineiras de forma semi-automática. Com isto, a barreira de entrada baixa bastante para teóricos “clássicos”.

O papel está a deslocar-se: as pessoas trazem ideias, estratégias e intuição - a máquina vigia a lógica sem concessões.

Para a próxima geração de estudantes, pode tornar-se normal não só escrever provas com giz no quadro, mas também formalizá-las em paralelo em Lean ou Coq.

O que esta evolução significa para o futuro da matemática

A colaboração estreita com software está a alterar o auto-entendimento da disciplina. Quando um computador aceita uma prova, esse enunciado fica assente num terreno mais firme do que muito do que, até hoje, passou apenas pelo crivo humano. Isto pode reorientar prioridades: em vez de gastar incontáveis horas na verificação manual de detalhes, os investigadores poderão canalizar mais energia para ideias novas e para estratégias de ataque.

Ao mesmo tempo, surgem perguntas inevitáveis: quanta confiança devemos depositar no próprio código dos “Proof Assistants”? Quem valida os programas que validam as nossas provas? Aqui entra um segundo nível de formalização: a lógica central destes sistemas pode ser verificada noutros instrumentos, reduzindo o risco de erros no alicerce.

Também são relevantes as possíveis aplicações fora da teoria pura: matemática correctamente verificada fornece base para criptografia, segurança de protocolos e estabilidade de algoritmos complexos. Se um “Proof Assistant” confirma uma prova de segurança, isso pode ter efeitos directos em métodos de encriptação ou na fiabilidade de software industrial.

Ainda há muito a ser construído, mas a direcção é inequívoca: a matemática está a tornar-se um palco partilhado por pessoas e máquinas. Os saltos criativos continuam a vir de investigadores de carne e osso. A fiscalização pedante e sem lacunas passa cada vez mais para o computador. Em conjunto, estas duas forças poderão permitir teoremas tão extensos e intrincados que nenhum cérebro humano, sozinho, conseguiria abarcar por completo.

---