3. Lógica
O capítulo tem três seções. Em Proof vamos usar Lean como assistente de prova, entendendo como usar o tipo Prop e como construir provas de proposições a partir de termos ou táticas. Em PL trataremos da implementação de lógica proposicional usando Lean como linguagem de programação, daremos a sintática e semântica de PL. Finalmente, em FOL, vamos implementar a lógica de predicados, novamente com sua sintaxe e semântica computável.