Euler's Eyes
2026-10-26
Notação para máquinas: provas que o computador confere
Durante dois mil anos, uma prova matemática foi um texto escrito para ser lido por pessoas. Ela podia pular passos “evidentes”, apoiar-se num desenho, usar convenções da comunidade. O leitor completava o resto. Nos últimos cinquenta anos, apareceu um leitor que não completa nada: o computador.
As quatro cores
Quantas cores bastam para pintar qualquer mapa de modo que países vizinhos tenham cores diferentes? A resposta, quatro, foi conjecturada em 1852 e resistiu mais de um século. Em 1976, Kenneth Appel e Wolfgang Haken, da Universidade de Illinois, a demonstraram reduzindo o problema a quase dois mil casos que um computador verificou um por um, em mais de mil horas de máquina.
A comunidade se dividiu. Uma prova que nenhum ser humano consegue ler inteira é uma prova? Os defensores lembravam que muitas provas longas também não são lidas por inteiro por ninguém; os críticos, que um programa pode ter erros. Em 2005, o francês Georges Gonthier escreveu a prova inteira, inclusive a parte do computador, num assistente de prova chamado Coq, que confere cada passo lógico a partir dos axiomas. A dúvida mudou de lugar: não era mais “o programa está certo?”, mas “o verificador está certo?”, um programa muito menor e mais fácil de auditar.
A conjectura de Kepler
Em 1611, Kepler afirmou que a maneira mais densa de empilhar laranjas é a pirâmide dos feirantes. Em 1998, o americano Thomas Hales anunciou uma prova que combinava centenas de páginas com cálculos extensos de computador. Uma equipe de árbitros trabalhou quatro anos e declarou estar “99% certa” da correção. Hales não se conformou com o 1% e começou o projeto Flyspeck para escrever a prova inteira numa linguagem formal. Em 2014, com dezenas de colaboradores, o projeto terminou: a máquina conferiu cada passo.
Lean
O assistente de prova mais usado hoje pelos matemáticos é o Lean, criado em 2013 pelo brasileiro Leonardo de Moura, então na Microsoft Research. Em torno dele cresceu a mathlib, uma biblioteca coletiva com centenas de milhares de teoremas formalizados, escritos por centenas de pessoas. Em 2020, o alemão Peter Scholze, medalhista Fields, desafiou a comunidade a formalizar um resultado seu que ele próprio não tinha certeza de ter verificado em todos os detalhes. O Liquid Tensor Experiment terminou em 2022: o resultado estava certo, e a formalização encontrou simplificações na prova.
Uma linha de Lean se parece com isto:
theorem soma_comuta (a b : ℕ) : a + b = b + a := Nat.add_comm a b
“Para quaisquer naturais $a$ e $b$, $a + b = b + a$, e a prova é o teorema da comutatividade da biblioteca.” Nada fica subentendido: o tipo de cada letra, a origem de cada passo. É a escrita linear do capítulo 7 levada ao extremo, e a prova com palavras do capítulo 4 traduzida para uma gramática que uma máquina consegue checar.
Exercício: quando três cores não bastam
Um país central é cercado por três países, e cada um desses três faz fronteira com os outros dois. Mostre que esse mapa precisa de quatro cores.
Os quatro países fazem fronteira dois a dois: o central toca os três, e os três se tocam entre si. Então cada um precisa de uma cor diferente de todos os outros, e são necessárias quatro. O teorema garante que nunca são necessárias cinco, por mais complicado que seja o mapa.
Exercício: leia a linha de Lean
Na linha theorem soma_comuta (a b : ℕ) : a + b = b + a := Nat.add_comm a b, identifique a hipótese, o enunciado e a prova.
(a b : ℕ) declara as letras: $a$ e $b$ são números naturais, como o “sejam $a$ e $b$ naturais” de um texto. Depois dos dois-pontos vem o enunciado, $a + b = b + a$. Depois de := vem a prova, que aqui é só a referência a um teorema já provado na biblioteca. O := do Algol, que vimos no texto 5, reaparece com um sentido novo: “é definido como”, ou “é provado por”.
Índice do capítulo · ← Na vida dez, na escola zero: a matemática fora do papel · Notação e cultura: roteiro e glossário →