Topic outline

  • General

     

    example Lean code

     
    Spring 2025, teaching periods IV-V
     

    Teachers
     
    • Kalle Kytölä (lecturer)
    • Janette Setälä (teaching assistant)

    Practicalities
    • The lectures will be held on Thursdays 14-16 in Y427a. See the Lectures tab for more details.
    • The exercise classes will be held on Mondays 14-16 in Y427a. See the Exercises tab for more details.
    Note that the lecture and exercise class times are effectively swapped with each other from those announced in Sisu. The content in both is similar; the main difference is that in exercise classes there is more emphasis on solving exercises and getting help with questions you have on them.
     
     
    Description of the course
     
    Computer formalization of mathematics is an emerging trend, which might in the future significantly affect mathematics research, teaching, and collaboration (as well as potentially even the role of AI in mathematics). This course introduces you to the basics of a formal language of mathematics, computer verified proofs in an interactive theorem prover, and libraries and tools for the formalization of mathematics. The goal is to learn to work with standard mathematics (algebra, topology, analysis, ...) at the level of logical precision required in a fully formal language. In the second half of the course, participants undertake small formalization projects.
     

    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 some mathematical maturity and willingness to work with a computer. 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 exercises in the first half of the course and doing a formalization project in the second half of the course.