Importância do rigor em provas matemática e papel dos Proofs Assistants. Básicos de Lean, Isabelle e Lean. Prova da infinitude dos números primos em cada um.