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 general-purpose 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 domain-specific languages supporting features like probabilistic programming or write programs that are guaranteed to be differentiable.

In the past, many specialized domain-specific 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.

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.

Markus Himmel: Working with Mathlib

One of Lean's great strengths is its mathematical library, mathlib. It covers almost all undergraduate and some graduate-level 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.

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 so-called "metaprogramming". Applications of this include extending the syntax to more faithfully represent the mathematical literature, writing custom proof automation (both general-purpose 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 low-level details of the system. In this presentation, I will give an overview over the various ways of extending Lean and give examples of user-defined 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.

Pietro Monticone: Getting Started with Blueprint-Driven 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 real-world, collaborative, blueprint-driven formalization projects in Lean, requiring almost no prior knowledge of Git, GitHub, continuous integration systems, or other commonly used technical tools.