Lean Theorem Prover

Minhas anotações sobre o uso do Lean para realizar provas formais de matemática e lógica proposicional. O Lean é uma linguagem funcional e um assistente de prova baseado na teoria de tipos dependentes.

Objetivo do Estudo

Explorar como formalizar teoremas simples e verificar a validade de argumentos lógicos de forma automática. Atualmente, o foco está em:

• Lógica proposicional básica (implicação, conjunção e negação).
• Provas de relações de subconjuntos e funções.
• Uso de táticas como intro, apply e exact.

Exemplo de Código

Abaixo, um exemplo simples de uma prova de identidade em lógica proposicional:

-- Exemplo de prova simples em Lean 4
theorem my_proof (p q : Prop) : p ∧ q → q ∧ p :=
begin
  intro h,
  cases h with hp hq,
  split,
  exact hq,
  exact hp,
end