2024-08-04, 10:45–11:15 (Asia/Taipei), TR514
Yuki Otsuka provides an overview of Lean4 and provides materials and tools to help you learn. Lean4 is an open-source theorem-proving support system and an environment that can also be used as a programming language. His presentation will not be an industrial introduction to the theorem-proving support system but will be introducing Lean4 as an environment for learning logic and mathematics through Lean4.
Yuki Otsuka presents the Lean4 theorem-prover from its historical background. He compares it to other theorem provers and points out what makes Lean4 stand out. His presentation includes his online resources selected to improve the learning of logic and mathematics through Lean4.
Yuki Otsuka is a Japanese university student with a strong interest in open-source technologies, programming languages, programming language theory, and programming language type systems. He is a member of the Japan openSUSE user group and served as a volunteer staff member at the Linux Foundation's Open Source Summit Japan.