Topic outline

  • General

     

    example Lean code


    Spring 2025, teaching periods IV-V

    Teachers

    Lecturer:
    • Kalle Kytölä

    Practicalities
    • The lectures will be held on Mondays 14-16 in Y427a. See the Lectures tab for more details.
    • The exercise classes will be held on Thursdays 14-16 in Y427a. See the Exercises tab for more details.

    Description of the course
    More information will be added later.


    Course contents and learning objectives

    Key topics of the course include:

    • formal language of mathematics and computer verified proofs in an interactive theorem prover (a proof assistant), libraries and tools for the formalization of mathematics

    Upon successful completion of this course, you will be able to. . .
    • . . . write basic formal mathematical statements and proofs in Lean4 interactive theorem prover; 
    • . . . use the libraries and tools of Lean4 to construct and inspect proofs;
    • . . . participate in formalization projects or run projects of your own.


    Prerequisites

    The course mainly requires willingness to work with a computer, and some mathematical maturity. For example, the participants should be familiar with most of the content and the ways of mathematical thinking in the following undergraduate mathematics courses:

    MS-C1081 Abstract Algebra

    MS-C1541 Metric Spaces


    Completing the course
    The course is completed by solving and participanting in exercises in the first half of the course, and doing a formalization project in the second half of the course.