Este minicurso introdutório apresenta o assistente de provas Lean 4 e a biblioteca Mathlib, mostrando o aspecto do Lean como linguagem de programação funcional e como ferramenta de verificação formal de demonstrações matemáticas. Ao longo dos encontros, os participantes serão conduzidos da sintaxe básica e dos fundamentos lógicos do sistema até a formalização de propriedades de espaços vetoriais e de convergência de sequências reais, com prática direta em jogos interativos de formalização. O curso utiliza o ambiente Lean Web, dispensando instalação local. Ao final, o participante será capaz de ler e escrever demonstrações formais simples e de compreender o papel da verificação interativa de provas realizada pelo Lean.