LEARNING OUTCOMES
After this course, you will be able to (1) write basic formal mathematical statements and proofs in Lean4 interactive theorem prover; (2) use the libraries and tools of Lean4 to construct and inspect proofs; (3) participate in formalization projects or even run projects of your own.Credits: 5
Schedule: 24.02.2025 - 26.05.2025
Teacher in charge (valid for whole curriculum period):
Teacher in charge (applies in this implementation): Kalle Kytölä
Contact information for the course (applies in this implementation):
CEFR level (valid for whole curriculum period):
Language of instruction and studies (applies in this implementation):
Teaching language: English. Languages of study attainment: English
CONTENT, ASSESSMENT AND WORKLOAD
Content
valid for whole curriculum period:
formal language of mathematics and computer verified proofs in interactive theorem prover (a.k.a. proof assistant), libraries and tools for the formalization of mathematics
Assessment Methods and Criteria
valid for whole curriculum period:
exercises, project
Workload
valid for whole curriculum period:
lectures, exercises, project
DETAILS
Study Material
valid for whole curriculum period:
Online textbook “Mathematics in Lean” <https://leanprover-community.github.io/mathematics_in_lean/> and material provided during the course
Substitutes for Courses
valid for whole curriculum period:
Prerequisites
valid for whole curriculum period:
FURTHER INFORMATION
Further Information
valid for whole curriculum period:
Teaching period: IV-V (Spring 2025)