Provar teoremas é um trabalho difícil. No fim do Séc. XVIII, Leibniz ambicionava encontrar uma linguagem universal que pudesse exprimir toda a proposição matemática e um método mecânico de cálculo que permitisse, sobre essa linguagem, calcular mecanicamente a prova de todos os teoremas. Uma enorme quantidade de esforço foi dispendida por muitos matemáticos na procura deste método que reduziria a procura da Verdade matemática à aplicação de um conjunto de regras tipográficas. Gödel demonstrou que isto é impossível e que toda a tentativa de o fazer está destinada a falhar: a Verdade matemática - seja lá o que isso for - não pode ser capturada pelos conceitos áridos de axioma e regra lógica. Fazer matemática não é só fazer contas - nem nunca poderá vir ser. Este seminário contará a história e dará uma ideia da prova desta demonstração.