Lecture
This lecture introduces the LISA proof assistant, focusing on its codebase organization, the kernel package containing trusted code for theorem production and proof verification, the FOL package for First Order Logic formalization, and the proof package built on top of FOL for defining sequents, proof steps, and theorems.