Software e Proof-Assistants na matemática: Lean, Coq e Isabelle encontram erros invisíveis

Em meio à matemática, o software entrou em cena - e passou a localizar falhas que ninguém conseguia enxergar.

Durante muito tempo, em salas silenciosas entre quadros de giz e cadernos, vigorou uma regra não escrita: um teorema é tão confiável quanto a confiança que os melhores especialistas depositam no seu argumento. Só que essa lógica vem perdendo força. Cada vez mais pesquisadores de ponta colocam seus resultados para serem verificados linha a linha por programas como Lean, Coq e Isabelle. O que antes era sustentado por reputação e leitura atenta vira lógica formal auditável em código; o trabalho solitário dá lugar a esforços em rede.

Do gênio solitário ao projeto em rede

Por séculos, a pesquisa em matemática seguiu quase sempre o mesmo roteiro: uma pessoa (ou um grupo pequeno) desenvolve uma ideia de prova, redige o texto, envia a uma revista, e então colegas passam meses lendo e relendo. No melhor cenário, ninguém encontra uma brecha. No pior, anos depois aparece um erro que derruba tudo.

Essa insegurança também alcançou Peter Scholze, um dos matemáticos mais conhecidos da Alemanha e vencedor da Medalha Fields. Em 2018, ele publicou uma prova altamente complexa sobre os chamados “espaços compactos”, apresentada numa formulação nova e extremamente abstrata. No mundo inteiro, apenas um punhado de pessoas conseguiria acompanhar o raciocínio. O próprio Scholze não tinha certeza absoluta de que algum deslize minúsculo não tivesse escapado.

Em vez de pedir mais pareceres, ele optou por um caminho radical: lançou publicamente o “Liquid Tensor Experiment”. A proposta era simples e exigente ao mesmo tempo: quem dominasse a linguagem de prova Lean deveria tentar formalizar integralmente a argumentação nessa linguagem. Nada de texto solto; apenas código rigorosamente estruturado, legível por máquina e passível de checagem automática.

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

Depois de cerca de seis meses, um time internacional anunciou o resultado: por volta de 180.000 linhas de código Lean cobriam toda a argumentação - sem lacunas lógicas. Para Scholze, isso representou um padrão de qualidade diferente de qualquer avaliação tradicional. Para a comunidade, foi um divisor de águas: um ofício milenar passou a funcionar, de uma vez, como uma empreitada coletiva apoiada por computador.

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

O caso de Scholze não ficou isolado. Há outro exemplo de grande repercussão: a matemática ucraniana Maryna Viazovska resolveu um enigma antigo sobre o empacotamento mais denso de esferas em oito dimensões - um problema altamente abstrato que ficou em aberto por séculos. A solução lhe rendeu, em 2022, a Medalha Fields.

A arquitetura da prova era brilhante, mas tão compacta e técnica que uma checagem completa apenas manual poderia consumir anos. Por isso, um grupo de pesquisadores decidiu traduzir o trabalho para Lean. Durante meses, eles dividiram 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 garantido também numa forma formal, legível por máquina.

O ponto mais transformador dessa tecnologia aparece aqui: provas antes tratadas como “longas demais”, “técnicas demais” ou “na prática, não verificáveis” podem ser quebradas em partes, virando projetos editáveis e distribuídos.

• Teoremas extremamente extensos podem ser decompostos em muitos blocos pequenos.
• Equipes em vários continentes trabalham em paralelo em diferentes trechos.
• No fim, a máquina junta todas as peças e valida a lógica do conjunto.

Um componente central desse ecossistema é a Mathlib, a 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 crescente, em vez de refazer tudo do zero. Isso acelera projetos de forma significativa e reduz a barreira de entrada.

Quando o computador corrige um vencedor da Medalha Fields

Esses programas não servem apenas para confirmar provas corretas. Eles também expõem fragilidades que até especialistas deixam passar. Em 2021, pesquisadores formalizaram em Lean um resultado já premiado. O trabalho era reconhecido, um prêmio havia sido concedido, e a reputação estava estabelecida.

Ao converter a prova para código, o Lean travou num passo intermediário: faltava uma condição, e a cadeia lógica não estava completamente fechada. Nenhuma revisão humana tinha notado a inconsistência antes. Os autores precisaram ajustar a argumentação e escrever de forma mais precisa.

Isso ajuda a entender a natureza dessas ferramentas. Enquanto uma leitora humana, diante de uma prova de 100 páginas, pode se cansar ou “passar batido” por hábito, o software não aceita saltos. Toda variável precisa de definição explícita; toda conclusão tem de estar justificadamente ancorada. O efeito prático é reduzir atalhos informais e aumentar a robustez da lógica demonstrável.

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

Como proof-assistants mudam o dia a dia da matemática

Por muito tempo, esses sistemas foram vistos como brinquedos de informáticos teóricos. Para usá-los, era preciso saber programar, ter paciência e tolerar frustrações. Esse quadro está mudando rapidamente.

Interfaces mais modernas e assistentes apoiados por IA têm removido boa parte das barreiras. Modelos de linguagem sugerem trechos de código Lean quando pesquisadores descrevem uma etapa do rascunho feito à mão. Ambientes interativos mostram em tempo real se um passo é formalmente válido ou se ainda faltam hipóteses. Assim, doutorandas e doutorandos conseguem aprender, passo a passo, como converter intuição matemática em código preciso.

O que Lean, Coq e Isabelle realmente fazem

Todas essas ferramentas pertencem à categoria dos chamados assistentes de prova. O princípio central é o seguinte:

• Afirmações matemáticas são convertidas para uma linguagem formal estrita.
• O programa opera com um conjunto fixo de regras de lógica e de inferência permitidas.
• Cada etapa de uma prova precisa ser justificável segundo essas regras.
• Se houver um salto ou uma lacuna em algum ponto, o processo de prova é interrompido.

Em vez de “inventar” automaticamente uma prova inteira, esses programas acompanham a pessoa durante a construção. Eles podem sugerir caminhos intermediários, checar hipóteses ou indicar alternativas quando uma abordagem encalha. No melhor cenário, surge um diálogo: de um lado, a intuição; do outro, a exigência de rigor formal.

Oportunidades, riscos e questões em aberto

Os ganhos são evidentes: mais segurança de que resultados publicados realmente se sustentam. Verificação mais rápida de projetos muito complexos. Rastreabilidade maior, já que cada passo fica explicitado no código.

Ao mesmo tempo, aparece uma pergunta delicada: até onde a comunidade pode se apoiar nesses programas? Em algum momento, pesquisadores vão apenas conferir se o computador “ficou verde”, sem entender cada etapa? Há quem alerte para uma espécie de “matemática no piloto automático”, na qual só poucos especialistas conseguem compreender a fundo o código das próprias ferramentas.

Também pesa a dependência de plataformas e linguagens específicas. Quem constrói uma carreira baseada em provas no Lean se vincula a um ecossistema. O que acontece se a comunidade migrar, no futuro, para outro sistema? Esse tipo de dúvida aparece cada vez mais em debates técnicos.

O que muda para estudantes e docentes

Em muitas universidades, disciplinas de provas formais e de assistentes de prova têm entrado no currículo. Estudantes aprendem, além de estratégias clássicas, como codificar argumentos de modo formal. Isso aprofunda a compreensão: quando alguém é forçado a escrever explicitamente cada afirmação “óbvia”, fica claro onde antes existia apenas sensação de entendimento, e não entendimento de fato.

Docentes veem nisso uma chance de trazer mais transparência. Questões de prova, por exemplo, podem vir acompanhadas de scripts simples em Lean, permitindo que quem aprende teste por conta própria se o raciocínio está logicamente consistente. Assim, o termo “prova”, que muitas vezes soa quase místico, vira um procedimento estruturado que dá para praticar passo a passo.

Como segue: criatividade humana, rigor de máquina

Muitos pesquisadores acreditam que, nos próximos anos, deve se consolidar um modelo mais dividido: pessoas criam novos conceitos, arriscam conjecturas ousadas e desenham estratégias gerais. Depois começa o trabalho de detalhamento no proof-assistant, com apoio de IA que reconhece padrões úteis a partir de milhões de linhas de código já existentes.

Especialmente na fronteira do conhecimento - onde provas passam de várias centenas de páginas ou chegam a milhares de linhas de código - essa combinação pode acelerar muito a área. Projetos antes considerados “arriscados demais” ou “trabalhosos demais” se tornam mais viáveis. Disso podem surgir teorias com complexidade muito além do que uma única mente conseguiria dominar por completo - e ainda assim aceitas como seguras, porque cada linha da lógica formal fica verificável.

Com isso, muda também a noção do que é uma prova. Ela deixa de ser apenas um texto elegante numa revista e passa a ser um artefato composto por narrativa, código e bibliotecas mantidas coletivamente. A imagem antiga do gênio sozinho à mesa cede espaço a equipes conectadas que, junto com software, trabalham no limite do que é possível demonstrar em matemática.

---