Os matemáticos não conseguem chegar a acordo acerca do que significa realmente “igual” — e isso é (literalmente) um problema. Uma nova teoria explora um conceito aparentemente simples, mas complexo.
O que é que significa 2+2=4? É complicado…
O matemático Kevin Buzzard tem estado na vanguarda da conversão de provas matemáticas clássicas em código verificável por computador, incluindo o famigerado Último Teorema de Fermat.
“Há seis anos, pensava que compreendia a igualdade matemática”, escreveu Buzzard no seu artigo, recentemente pré-publicado no arXiv.
“Pensava que era um termo bem definido, sem qualquer interesse para mim enquanto matemático ativo. Depois comecei a trabalhar com provadores de teoremas em computador e descobri que a igualdade era um conceito mais espinhoso do que eu pensava”.
Na programação, a igualdade não é tão simples como pode parecer na matemática tradicional. Existem diferentes tipos de igualdade e os programadores têm de definir meticulosamente cada passo que a intuição humana muitas vezes ignora. Por exemplo, num sistema de álgebra computacional, a cadeia “2 + 2” não é igual à cadeia “4”.
O artigo de Buzzard realça estas nuances, como por exemplo se o sinal de igual deve ter em conta os valores arredondados ou a passagem do tempo em equações dinâmicas.
“A utilização atual do sinal de igual na matemática é um pouco ‘solta‘“, diz Buzzard, citado pela New Scientist.
O matemático explica que, na prática, os matemáticos se baseiam muitas vezes numa intuição profunda e não numa estrutura lógica rigorosa. No entanto, nos verificadores de teoremas informáticos, como o sistema Lean, cada passo tem de ser explicitamente definido.
O trabalho de Buzzard consiste em traduzir provas matemáticas escritas por humanos em algoritmos pormenorizados que os computadores possam compreender e verificar.
Um exemplo ilustrativo que Buzzard usa é o trabalho do matemático Alexander Grothendieck, que introduziu o termo “canonicamente isomórfico” para descrever uma nova forma de igualdade.
No sistema Lean, esta nova forma seria assinalada como incorreta, realçando a diferença entre a intuição matemática tradicional e a precisão exigida pelas provas informáticas.
Buzzard conclui que transformação da matemática em código e provas formais requer a resolução de muitas lacunas e “buracos” nos métodos atuais. Este processo de formalização pode beneficiar significativamente os matemáticos que constroem bibliotecas em software como o Lean.
Buzzard sugere que um truque que os matemáticos usam é “abusar” do símbolo de igualdade, fazendo-o significar algo que não significa. No entanto, no domínio da codificação informática, esses atalhos não são permitidos.
E então, o que é que significa 2+2=4? É complicado…
