Prova

Definição

Sequência finita de proposições onde cada uma é um axioma, uma hipótese, ou consequência das anteriores por regras de inferência, terminando na proposição a demonstrar.

Intuição

O caminho da derivação. Não é "convencer alguém" — é exibir a rota formal do ponto A (axiomas) ao ponto B (teorema).

Registro computacional

Pelo isomorfismo de Curry-Howard, uma prova é um programa. Prova e programa são literalmente a mesma coisa em sintaxes diferentes.