Revolução no laboratório de matemática: agora é o software que avalia as provas

Durante anos, a matemática viveu quase à margem do software: os resultados eram julgados sobretudo pelo olhar humano, pela reputação das equipas e pela paciência de quem lia cada linha. Agora, esse equilíbrio está a mudar. Programas como Lean, Coq ou Isabelle passam os teoremas a pente fino e conseguem detetar falhas que escapavam até a especialistas experientes.

O que antes dependia de confiança entre pares está a transformar-se num processo de verificação formal. Em vez de um pequeno grupo de génios a trabalhar isoladamente, surgem equipas ligadas por código, bibliotecas partilhadas e uma regra simples: um argumento só conta se puder ser confirmado passo a passo por uma máquina.

Vom einsamen Genie zum vernetzten Projekt

Durante séculos, a investigação matemática seguiu praticamente o mesmo roteiro: uma pessoa ou uma pequena equipa trabalha uma ideia, escreve a demonstração, envia-a para revistas científicas e depois colegas vão lendo durante meses. Com sorte, não aparece nenhuma falha. Com azar, anos mais tarde alguém descobre um erro e deita tudo por terra.

Essa incerteza também atingiu Peter Scholze, um dos matemáticos alemães mais conhecidos e medalha Fields. Em 2018, publicou uma prova altamente complexa sobre os chamados “espaços compactos”, numa formulação nova e extremamente abstrata. Só um punhado de pessoas no mundo conseguia sequer acompanhá-la. O próprio Scholze não tinha a certeza absoluta de que não existisse algum deslize subtil escondido algures.

Em vez de pedir mais pareceres, escolheu um caminho radicalmente novo: lançou publicamente o “Liquid Tensor Experiment”. A ideia era simples na teoria, exigente na prática: quem dominasse o software de prova Lean devia tentar formalizar toda a argumentação nessa linguagem. Ou seja, nada de texto solto - apenas código rigidamente estruturado, compreendido e verificado por uma máquina.

Um teorema só passa a valer neste novo cenário quando não são apenas pessoas, mas também um algoritmo rigoroso, a aprovar cada linha.

Ao fim de cerca de seis meses, uma equipa internacional anunciou sucesso: cerca de 180 mil linhas de código Lean cobriam toda a argumentação, sem lacunas lógicas. Para Scholze, foi um nível de qualidade diferente de qualquer revisão clássica. Para a comunidade, foi um momento decisivo: um ofício com raízes milenares passou, de repente, a ser um esforço coletivo e assistido por computador.

Software torna provas aparentemente “inverificáveis” controláveis

O caso Scholze não ficou isolado. Outro exemplo de destaque: a matemática ucraniana Maryna Viazovska resolveu um problema antigo sobre o empacotamento mais denso de esferas em oito dimensões - um tema altamente abstrato, em aberto há séculos. A sua solução valeu-lhe também a medalha Fields, em 2022.

A estrutura da demonstração era brilhante, mas tão compacta que uma verificação manual completa teria levado anos. Por isso, um grupo de investigadores decidiu traduzi-la para Lean. Durante meses, foram decomposto cada trecho em passos lógicos ainda mais pequenos, até que a prova inteira ficou disponível como programa. Em 2024, o código completo foi publicado no GitHub - e a demonstração passou a estar também assegurada, em forma formal e legível por máquina.

Isto mostra a verdadeira força desta tecnologia: provas que antes eram consideradas “demasiado longas”, “demasiado técnicas” ou “praticamente impossíveis de confirmar” podem, afinal, ser divididas em subprojetos geríveis.

• Teoremas extremamente extensos podem ser repartidos em muitos blocos pequenos.
• Equipas em vários continentes trabalham em paralelo em partes diferentes.
• No fim, a máquina junta todas as peças e valida a lógica global.

Um papel central cabe ao Mathlib, a grande biblioteca standard do Lean. Hoje já reúne mais de um milhão de linhas de definições formalizadas e teoremas demonstrados. Cada nova prova pode apoiar-se nessa base crescente, em vez de começar do zero. Isso acelera imenso os projetos e reduz a barreira de entrada.

Quando o computador corrige um medalhado Fields

Estes programas não servem apenas para confirmar demonstrações que já estão corretas à partida. Também expõem fragilidades que nem especialistas detetam. Em 2021, investigadores formalizaram em Lean um resultado já premiado. O trabalho era respeitado na área, o prémio tinha sido atribuído, a reputação estava consolidada.

Ao transpor a prova para código, o Lean travou numa construção intermédia: faltava uma condição, e a cadeia lógica não fechava de forma limpa. Nenhuma revisão humana tinha assinalado essa inconsistência antes. Os autores tiveram de ajustar a argumentação e formulá-la com mais precisão.

Isto mostra bem a natureza destas ferramentas novas. Enquanto um leitor humano, perante uma prova de 100 páginas, acaba por se cansar ou por passar por cima de um salto, o software não aceita atalhos. Cada variável precisa de definição clara, cada conclusão tem de ser justificada sem ambiguidades. O resultado é menos espaço para abreviações informais e mais lógica robusta e verificável.

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

Como os proof-assistants estão a mudar o dia a dia da matemática

Durante muito tempo, estes sistemas foram vistos como brinquedos para informáticos teóricos. Quem quisesse usá-los precisava de saber programar, ter muita paciência e alguma resistência à frustração. Isso está a mudar depressa.

Interfaces mais modernas e assistentes com IA estão a retirar grande parte dos obstáculos. Modelos de linguagem sugerem código Lean quando os investigadores descrevem uma parte da sua prova em linguagem natural. Ambientes interativos mostram em tempo real se um passo é formalmente válido ou se ainda faltam hipóteses. Assim, doutorandos e outras pessoas em formação podem aprender, passo a passo, a transformar ideias em código preciso.

O que Lean, Coq e Isabelle fazem afinal

Todas estas ferramentas pertencem ao grupo dos chamados proof-assistants. O princípio central é este:

• As afirmações matemáticas são convertidas para uma linguagem formal rigorosa.
• O software conhece um conjunto fixo de regras lógicas e de inferência permitidas.
• Cada passo de uma demonstração tem de ser rastreável segundo essas regras.
• Se houver um salto ou uma lacuna, o processo de prova pára.

Em vez de “inventarem” automaticamente uma prova completa, estes programas acompanham a pessoa na construção. Sugerem caminhos parciais, verificam hipóteses ou apontam alternativas quando uma abordagem entra num beco sem saída. No cenário ideal, cria-se um diálogo entre a intuição de um lado e o rigor formal do outro.

Oportunidades, riscos e questões em aberto

As vantagens são claras: mais segurança de que os resultados publicados realmente se sustentam; verificação mais rápida de projetos extremamente complexos; e melhor rastreabilidade, porque cada passo fica explícito no código.

Ao mesmo tempo, surge uma questão delicada: até onde pode a comunidade confiar neste software? Chegará o momento em que os investigadores só olham para o facto de o computador dar luz verde, sem compreenderem cada passo? Há quem alerte já para uma espécie de “matemática em piloto automático”, em que apenas alguns especialistas conseguem perceber o código interno destas ferramentas.

Acresce ainda a dependência de plataformas e linguagens específicas. Quem constrói a sua carreira sobre provas em Lean fica preso a um ecossistema. O que acontece se, um dia, a comunidade migrar para outro sistema? Estas perguntas aparecem cada vez mais nas discussões da área.

O que muda para estudantes e docentes

Em muitas universidades, os cursos de provas formais e proof-assistants já começam a entrar no plano curricular. Os estudantes aprendem, além das estratégias clássicas de demonstração, a codificar argumentos de forma formal. Isso afina a compreensão: quem é obrigado a explicitar cada afirmação aparentemente “óbvia” percebe depressa onde antes só intuía, mas não entendia de facto.

Os docentes veem aqui uma oportunidade para dar mais transparência ao processo. Por exemplo, problemas de avaliação podem ser acompanhados por pequenos scripts em Lean, que permitem aos alunos testar por si próprios se os seus raciocínios são logicamente sólidos. Assim, o termo muitas vezes quase místico “prova” torna-se um processo claro e estruturado, treinável passo a passo.

Como vai evoluir: criatividade humana, rigor da máquina

Muitos investigadores acreditam que, nos próximos anos, se vai consolidar um modelo de trabalho repartido: as pessoas criam novos conceitos, arriscam conjecturas ousadas e esboçam estratégias gerais. Depois, começa o trabalho minucioso no proof-assistant, 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 as demonstrações podem ter várias centenas de páginas ou milhares de linhas de código, esta combinação pode impulsionar a disciplina de forma decisiva. Projetos que antes pareciam “demasiado arriscados” ou “demasiado trabalhosos” tornam-se mais realistas. Daí podem surgir teorias cuja complexidade ultrapassa largamente aquilo que uma única mente conseguiria acompanhar por completo - e que, ainda assim, passam a ser consideradas seguras porque cada linha de lógica formal é verificável.

Com isso, também muda a própria definição do que é uma prova. Já não é apenas um ensaio elegante numa revista científica, mas uma construção feita de texto, código e bibliotecas mantidas em conjunto. A velha imagem do génio solitário à secretária dá lugar a equipas ligadas em rede, a trabalhar com software na fronteira do demonstrável em matemática.