About this event:
Formalisation is the process of specifying a mathematical proof in sufficient detail so that a computer program can verify its correctness automatically. Formal proofs have a number of advantages beyond the verification of the correctness of the theorem.
Lean is a software system for carrying out proof formalisations. Due to a number of recent successes, such as the liquid tensor experiment, the formalisation of proofs in Lean has received considerable attention in the mathematical community.
The intended audience of this tutorial are mathematicians from all research areas who are curious about this topic. There will be several talks, given by Lean experts, to explain the basics and provide examples, as well as practice sessions, where participants will use Lean in real world situations on their own laptops.
Date and Venue:
The tutorial will take place on September 1820, 2024 in the Seminarraum Argentinierstraße at TU Wien in Vienna, Austria.Speakers / Tutors:
 Martin Dvořák, Institute of Science and Technology Austria (ISTA)
 Moritz Firsching, Google Research Zürich
 Markus Himmel, Lean FRO
 Pietro Monticone, University of Trento
 Tomáš Skřivan, Carnegie Mellon University
Registration:
The registration is closed now. The registration deadline was August 31, 2024.Programme:
The programme contains two different kinds of sessions. On the one hand, there will be tutorial sessions which include presentations of basic aspects of Lean and practice sessions where the participants will use Lean on their own laptops. On the other hand, there will be research presentations which cover more advanced topics and current research.
We have setup a github repository with resources for this tutorial.
Wednesday, September 18, 2024 


9:00  10:00 
Markus Himmel: Introduction to Lean 
10:00  10:30 
Coffee Break 
10:30  12:00 
Pietro Monticone: Installation and Basics 
12:00  13:30 
Lunch Break 
13:30  14:15 
Tomáš Skřivan: Scientific Computing in Lean The language of science is mathematics and Lean speaks mathematics. Since Lean 4 is an interactive theorem prover and generalpurpose programming language simultaneously, it is only natural to explore its use for scientific computing. At first glance, the advantage of using Lean is that we can fully formalize and prove the correctness of our programs. However, we will show that the utility of using an interactive theorem prover goes far beyond that. The ability to express abstract mathematical concepts allows us to build a library with an extremely high level of composability. We utilize Lean’s interactivity and tactic mode to create an interactive computer algebra system, perform source code transformations, or execute compiler optimization passes. Lean’s extensible syntax allows us to define custom domainspecific languages supporting features like probabilistic programming or write programs that are guaranteed to be differentiable. In the past, many specialized domainspecific languages have been developed to support one of these features. Our aim is to develop a language/library where all these specialized features can coexist seamlessly. 
14:15  15:30 
Pietro Monticone: Logic (1/2) 
15:30  16:00 
Coffee Break 
16:00  17:30 
Pietro Monticone: Logic (2/2) 
Thursday, September 19, 2024 


9:00  9:45 
Moritz Firsching: Beginner's mistakes using Mathlib/Lean This talk addresses the common pitfalls that beginners face when using Mathlib in Lean. With examples we show typical problems when navigating syntax and formulating theorems. We will explore these common mistakes, offering practical advice and solutions to help newcomers avoid them. In addition, we will discuss the challenges of discovering theorems within Mathlib and also cover effective strategies for debugging statements and interpreting Lean error messages. 
9:45  10:15 
Coffee Break 
10:15  12:15 
Markus Himmel: Sets and Functions 
12:15  13:45 
Lunch Break 
13:45  14:30 
Markus Himmel: Working with Mathlib One of Lean's great strengths is its mathematical library, mathlib. It covers almost all undergraduate and some graduatelevel mathematics and forms the base on which all mathematical formalization projects using Lean build. At 1.5 million lines of code, being able to navigate mathlib efficiently and find relevant results quickly is an important skill. There are many useful tools to assist with this, and in this presentation I will give a practical demonstration of these tools in action. 
14:30  15:45 
Moritz Firsching: Elementary Number Theory (1/2) 
15:45  16:15 
Coffee Break 
16:15  17:30 
Moritz Firsching: Elementary Number Theory (2/2) 
Friday, September 20, 2024 


9:00  9:30 
Markus Himmel: Lean Metaprogramming Overview One of Lean's unique features is the breadth and depth of possibilities for users to shape and extend the language through socalled "metaprogramming". Applications of this include extending the syntax to more faithfully represent the mathematical literature, writing custom proof automation (both generalpurpose and tailored to specific mathematical subject areas or even single proofs), and adding new visualisations (for example string diagrams) to the Lean InfoView. Many of these applications are accessible without any programming knowledge, while advanced users have access to even the most lowlevel details of the system. In this presentation, I will give an overview over the various ways of extending Lean and give examples of userdefined extensions in action. My aim is to give participants an idea of what is possible (and how easy or difficult it is to learn the various aspects of metaprogramming) and point them to good learning resources if desired. 
9:30  10:30 
Tomáš Skřivan: Structures (1/2) 
10:30  11:00 
Coffee Break 
11:00  12:15 
Tomáš Skřivan: Structures (2/2) 
12:15  13:45 
Lunch Break 
13:45  14:30 
Pietro Monticone: Getting Started with BlueprintDriven Formalisation Projects in Lean Intended for mathematicians at all levels, this talk aims to provide a practical and comprehensive introduction to the design, management, and implementation of realworld, collaborative, blueprintdriven formalization projects in Lean, requiring almost no prior knowledge of Git, GitHub, continuous integration systems, or other commonly used technical tools. 
14:30  15:45 
Tomáš Skřivan: Differential Calculus (1/2) 
15:45  16:15 
Coffee Break 
16:15  17:30 
Tomáš Skřivan: Differential Calculus (2/2) 
Organisers:
 Stefan Hetzl, TU Wien
 Fabian Achammer, TU Wien
 Parham Shadman, TU Wien