Learning Mathematics with Lean

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

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.