Quando o software entra em cena - e encontra erros que ninguém conseguia enxergar

Por muito tempo, em escritórios silenciosos cheios de quadros de giz e cadernos rabiscados, vigorou uma regra não escrita: um teorema é tão confiável quanto os melhores especialistas que o leram e aprovaram. Só que esse período está perdendo força. Cada vez mais pesquisadores de ponta pedem que seus resultados sejam verificados, linha por linha, por programas como Lean, Coq e Isabelle. O que antes dependia sobretudo de confiança e reputação passa a ser sustentado por lógica verificável em código - e, com isso, a matemática deixa de ser um ofício de poucos para se tornar também um trabalho colaborativo, conectado e rastreável.

O que Lean, Coq e Isabelle realmente fazem (e por que isso importa)

Essas ferramentas pertencem à categoria dos assistentes de prova (proof assistants). A proposta central é simples, mas exigente:

• Enunciados matemáticos são convertidos para uma linguagem formal rigorosa.
• O sistema opera com um conjunto fixo de regras de lógica e inferência permitidas.
• Cada etapa da prova precisa ser justificável dentro dessas regras, sem “saltos”.
• Se houver uma lacuna, uma hipótese faltando ou um passo inválido, a verificação para ali.

Eles não “inventam” automaticamente uma prova completa do nada. Na prática, atuam como parceiros de construção: conferem hipóteses, aceitam (ou recusam) cada transição, sugerem caminhos intermediários e, quando um método encalha, ajudam a explorar alternativas. No melhor cenário, surge um diálogo produtivo: intuição humana de um lado, formalização implacável do outro.

Do gênio solitário ao projeto em rede com Lean

Durante séculos, a pesquisa em matemática seguiu um roteiro relativamente estável: uma pessoa (ou um grupo pequeno) desenvolve uma ideia, escreve um texto com argumentos e envia a uma revista. Depois, colegas leem por meses. Se ninguém detectar um furo, o resultado se estabelece - embora, às vezes, um erro só apareça muitos anos depois e obrigue a rever tudo.

Essa sensação de fragilidade também atingiu Peter Scholze, um dos matemáticos alemães mais conhecidos e ganhador da Medalha Fields. Em 2018, ele publicou uma demonstração extremamente sofisticada envolvendo espaços compactos, apresentada numa formulação nova e altamente abstrata. Tão abstrata, aliás, que apenas um grupo minúsculo no mundo conseguia acompanhar o raciocínio por completo. O próprio Scholze não se dizia totalmente tranquilo com a possibilidade de não existir, escondido em algum ponto, um deslize minúsculo.

Em vez de solicitar novas rodadas de pareceres tradicionais, ele adotou um caminho pouco convencional: anunciou publicamente o Liquid Tensor Experiment. A proposta era direta: quem dominasse o assistente de prova Lean deveria tentar formalizar a argumentação inteira nessa linguagem - não como um texto “solto”, mas como um código rigidamente estruturado, compreensível e verificável por uma máquina.

Nesse novo regime, um teorema só passa a ser aceito quando não apenas pessoas, mas também um algoritmo rigoroso aprova cada linha.

Após cerca de seis meses, um time internacional reportou sucesso: aproximadamente 180.000 linhas de código em Lean cobriam toda a cadeia de argumentos, sem brechas lógicas. Para Scholze, isso representou um nível de garantia diferente de qualquer avaliação convencional. Para a comunidade, foi um divisor de águas: um ofício milenar ganhou, de uma vez, uma camada coletiva e assistida por computador.

Tornando “impossível de checar” em algo controlável

O episódio com Scholze não virou exceção isolada. Outro caso emblemático envolve a matemática ucraniana Maryna Viazovska, que solucionou um problema clássico sobre a empacotamento mais denso de esferas em oito dimensões - uma questão extremamente abstrata que permaneceu aberta por séculos. O feito também lhe rendeu a Medalha Fields, em 2022.

A estrutura do argumento era brilhante, porém tão compacta e técnica que uma checagem manual completa poderia consumir anos. Por isso, um grupo de pesquisadores decidiu traduzir o trabalho para Lean. Ao longo de meses, cada seção foi “decomposta” em passos lógicos menores e menores, até que toda a prova existisse na forma de um programa. Em 2024, o código integral foi disponibilizado publicamente no GitHub - e a demonstração passou a existir também como um objeto formal, legível por máquina e verificável de ponta a ponta.

O ponto explosivo dessa tecnologia aparece aqui: provas antes consideradas “longas demais”, “técnicas demais” ou “na prática, impossíveis de revisar” começam a ser fatiadas em projetos administráveis.

• Teoremas gigantes podem ser divididos em blocos pequenos e bem definidos.
• Equipes distribuídas por continentes conseguem trabalhar em paralelo, cada uma numa parte.
• No final, a máquina conecta as peças e valida a consistência lógica do conjunto.

Nesse ecossistema, a Mathlib (a biblioteca padrão de Lean) ocupa um lugar central. Ela já reúne mais de um milhão de linhas de definições formalizadas e teoremas comprovados. Assim, novos projetos podem reaproveitar uma base crescente em vez de recomeçar do zero - o que acelera o desenvolvimento e diminui a barreira de entrada para quem está chegando.

Além disso, a formalização muda a própria logística do trabalho matemático: versões ficam registradas, mudanças são rastreáveis e é possível automatizar checagens contínuas (por exemplo, sempre que alguém altera um trecho do código, o sistema verifica se o restante ainda “fecha”). Esse tipo de disciplina - comum na engenharia de software - começa a se infiltrar no modo como provas complexas são mantidas e auditadas ao longo do tempo.

Quando o computador corrige até vencedores da Medalha Fields

Assistentes de prova não servem apenas para carimbar o que já está certo. Eles também expõem fragilidades que passam despercebidas até por especialistas. Em 2021, pesquisadores formalizaram em Lean um resultado já celebrado na área: o trabalho havia sido aceito, premiado e amplamente respeitado.

Só que, ao converter a prova em código, o Lean travou em um passo intermediário: faltava uma condição, e o encadeamento lógico não estava impecável. Nenhuma revisão humana anterior tinha percebido a inconsistência. Os autores precisaram ajustar a argumentação e redigir o ponto com muito mais precisão.

Isso evidencia uma diferença de comportamento: uma pessoa lendo uma prova de 100 páginas pode se cansar, pressupor detalhes “óbvios” ou seguir no embalo do estilo. Já o software não tolera pular etapas. Toda variável precisa estar definida, e cada conclusão tem de ser justificada de maneira estrita. O efeito prático costuma ser menos atalhos informais e mais lógica robusta, explicitamente verificável.

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

Como os assistentes de prova estão mudando o cotidiano da matemática

Por muito tempo, esses sistemas foram vistos como ferramentas de nicho, usadas principalmente por gente da informática teórica. Para adotá-los, era preciso saber programar, ter paciência e aceitar uma curva de aprendizado pesada. Isso está mudando rapidamente.

Interfaces mais modernas e recursos com IA reduzem uma parte grande do atrito. Modelos de linguagem conseguem sugerir trechos de código em Lean quando o pesquisador descreve um pedaço da prova em linguagem natural. Ambientes interativos exibem, em tempo real, se um passo está formalmente válido ou se ainda falta alguma hipótese. Para doutorandos e doutorandas, isso vira um aprendizado guiado: as ideias vão sendo convertidas em código com feedback imediato.

Ao mesmo tempo, cresce um debate sobre sustentabilidade: formalizar uma prova não é apenas “passar a limpo”. É um investimento que depende de bibliotecas, versões de linguagem e manutenção ao longo dos anos. Por isso, a discussão sobre padrões, compatibilidade e preservação (por exemplo, como manter verificável um projeto grande quando o ecossistema migra de versão) ganhou espaço junto com o entusiasmo.

O que muda para estudantes e docentes

Em muitas universidades, disciplinas de provas formais e assistentes de prova já entraram no currículo. Além de aprender técnicas clássicas de demonstração, estudantes passam a treinar como codificar argumentos de modo formal. Isso fortalece a compreensão: quando alguém é obrigado a escrever explicitamente até o que parecia “evidente”, descobre com rapidez onde estava apenas intuindo - e não entendendo de fato.

Para docentes, há uma oportunidade de trazer mais transparência para a avaliação. Exercícios podem vir acompanhados de scripts simples em Lean, permitindo que os próprios alunos testem se suas ideias estão logicamente completas. Assim, o conceito de “prova” deixa de soar como algo quase místico e vira um procedimento treinável, passo a passo, com critérios claros.

Oportunidades, riscos e perguntas em aberto

Os ganhos parecem óbvios: mais segurança de que resultados publicados realmente se sustentam; revisão mais rápida de projetos gigantescos; e rastreabilidade superior, porque cada etapa aparece explicitamente no código.

Ainda assim, há uma questão delicada: até que ponto a comunidade pode (ou deve) se apoiar nesses sistemas? Existe o risco de pesquisadores passarem a conferir apenas se o programa “ficou verde”, sem compreender profundamente os detalhes matemáticos? Alguns já alertam para uma espécie de “matemática no piloto automático”, na qual apenas um grupo reduzido entende a fundo o próprio funcionamento das ferramentas e bibliotecas.

Também pesa a dependência de plataformas e linguagens específicas. Quem constrói uma carreira com provas em Lean se liga a um ecossistema. E se, no futuro, a área migrar para outro sistema? Como ficam a portabilidade, o legado e a reprodutibilidade? Essas dúvidas aparecem com frequência crescente em debates técnicos.

Para onde isso aponta: criatividade humana, rigor de máquina

Muitos pesquisadores apostam que, nos próximos anos, vai se consolidar um modelo de trabalho mais dividido: pessoas criam novos conceitos, arriscam conjecturas ousadas e desenham estratégias gerais. Em seguida, entra a etapa de “granularidade fina” no assistente de prova, com apoio de IA capaz de reconhecer padrões e reutilizar estruturas aprendidas a partir de milhões de linhas já existentes.

Na fronteira do conhecimento - onde provas exigem centenas de páginas ou milhares de linhas de código - essa combinação tende a acelerar o avanço da disciplina. Resultados antes considerados “arriscados demais” ou “caros demais” se tornam mais viáveis. E podem surgir teorias com complexidade muito acima do que uma única pessoa conseguiria abarcar integralmente, mas ainda assim aceitas como sólidas porque cada linha de lógica formal fica disponível para verificação.

Com isso, muda também a noção do que é uma prova. Não apenas um texto elegante numa revista, e sim um artefato composto por explicação, código e bibliotecas mantidas coletivamente. A imagem do gênio solitário na escrivaninha cede espaço a equipes conectadas - trabalhando junto com software - no limite do que é demonstrável na matemática.