Titles & Abstracts

Stream: ItaLean 2025

[Pietro Monticone]

Hi everyone, we kindly ask each speaker to share below the title and abstract of their research or tutorial talk.

Of course, if you are giving more than one talk, please include separate entries for each.

[Filippo A. E. Nuccio]

[T] (Functional) Analysis in Mathlib
[A] In this tutorial I will explain how some usual constructions in calculus and analysis (most notably limits, derivatives and completeness) are formalised in Mathlib, showing how the language of filters allows for a uniform treatement even beyond these analytic concepts. I will then illustrate some applications of the above notions by drawing on some examples from the Functional Analysis library.

[Lorenzo Luccioli]

Hi everyone,
just a quick reminder to share the title of your talk here in the thread.

We already have a few entries, and it would help a lot with preparing the program if we could collect all titles soon.

If you already have an abstract ready, feel free to add it as well, otherwise the title is enough for now.

Thanks!

[Rémy Degenne]

I'm fine with the two titles you wrote for my talks. I'll prepare some abstracts soon(ish).

[Riccardo Brasca]

Sorry for the late answer.

Title: Number Theory in mathlib
Abstract: In this talk, I will explain how to work with the standard number-theoretic objects available in mathlib, such as number fields, ideal decomposition, and related algebraic structures. I will also give an overview of the current arithmetic capabilities of mathlib, highlighting what is already implemented, what remains challenging, and what developments can be expected in the near future.

[Michael Rothgang]

I'll create titles and abstracts for my two talks very soon.

[Damiano Testa]

Title
Metaprogramming in Lean

Abstract
I will give an introduction to metaprogramming in Lean, touching briefly upon Syntax, Expressions, InfoTrees and monadic programming.

I will prefer visualizations and examples over extensiveness and details. I assume no prior experience with metaprogramming.

[Michael Rothgang]

Title: Differential geometry in mathlib
Abstract: I'll give an introduction to differential geometry in mathlib. I will present the basic objects (such as charts, manifolds, smooth vector bundles and maps between them) and explain why mathlib differs from your average textbook. You'll get an overview over the current differential geometry library, including what is already present, what will be coming soon and how you can help. I discuss what is challenging and outline some development for making this easier.

[Michael Rothgang]

Title: The Carleson Project: Formalization and Collaboration

Abstract: In 1966 Lennart Carleson published a proof of an important theorem in harmonic analysis, that states that the Fourier series converges pointwise to the original function under weak conditions. This result has a notoriously difficult proof, and while the result has been generalized over the years, every found proof is full of intricate details.

I will describe a recently completed formalization project that verifies all the details of a generalized Carleson theorem in Lean. I will show a few learnings for formalising harmonic analysis and in particular reflect on the collaborative nature of this formalization.

[Rémy Degenne]

Title: Probability theory in Mathlib
Abstract: I will explain how to work with random variables and processes on probability spaces in Mathlib. I will give a tour of the probability notions and notable results available in the library and highlight areas that are currently under development. I will also focus on useful tactics and common proof patterns.

[Rémy Degenne]

Title: The Brownian Motion Project
Abstract: Brownian motion is a central objects of modern probability. I will report on a collaborative formalization project in which we built a Brownian motion in Lean, which involved proving the Kolmogorov extension theorem, facts about Gaussian measures, and the Kolmogorov-Chentsov continuity theorem. After we completed this goal, the focus of the project shifted to defining stochastic integrals, which is an ongoing effort. I will talk about the lessons we learned in the project about handling stochastic processes in Lean, and discuss the latest developments towards stochastic integrals.

[Leonardo de Moura]

Title: The Making of Lean

Abstract: Lean began in 2013 as an attempt to address the fundamental limitations I had encountered with Z3 and automatic theorem proving: proof instability, opaque failures, and the ceiling imposed by undecidability. What followed was twelve years of building, rebuilding, and occasionally fighting with the community that formed around the project. In this talk, I give a personal account of Lean's history, from early prototypes developed with Soonho Kong, through the growth of Lean 3 and the tensions it brought, to the years Sebastian Ullrich and I spent privately building Lean 4, and finally launching the Lean FRO together. I discuss what worked, what didn't, and the friends, colleagues, and volunteers who helped keep the project alive at critical moments. I conclude with a demo of grind, a new tactic that brings extensible SMT-style automation to dependent type theory, finally realizing Lean's original goal of unifying interactive and automated theorem proving.

[Emily Riehl]

Title: Challenges in (auto) formalizing category theory

Abstract: A distinctive feature of (classical 1-dimensional) category theory is that the definitions and theorem statements are hard but the proofs are easy. Once a result is stated at the correct level of abstraction, the proof can be found by following your nose. This talk will illustrate this principle with a few examples and then discuss its implications for computer formalization by either humans or AI.

[Alex Kontorovich]

Title: Lessons from the PNT+ Project and Real Analysis Game

Abstract: We will discuss some lessons learned from the PNT+ Project (complex analysis, large collaborative formalization, interactions with AI systems), and the Real Analysis Game (pedagogical aspects, technical aspects).

[Nehal Patel]

Title: The Three Horsemen: AI Agents know how to Lean

Abstract: The "Three Horsemen" (claude code, codex, and gemini) are AI agents that are transforming software development. They also are proficient in formal mathematics. Following a live demonstration, we will present an extremely simple recipe that solves 203 out of 660 Putnambench problems. We will also examine perturbations of this simple recipe and analyze the tools these agents use. Finally, we share some industry perspectives and discuss areas of potential collaboration.

[Moritz Firsching]

Title: The Formal Conjectures Project

Abstract: Despite the rapid growth of formalised mathematics, there remains a scarcity of open conjectures formalised solely as statements. The Formal Conjectures project aims to fill this gap, providing a benchmark for automated theorem provers and autoformalisation, as well as a resource for clarifying mathematical ambiguity. This presentation outlines the design and intention of the repository, detailing how open questions requiring an answer are formalised and how autoformalisation assists in this process. Furthermore, we discuss the symbiotic relationship between this resource and automated systems like AlphaProof. We highlight how the project enables these systems by serving as a testing ground, while simultaneously demonstrating how they contribute back by detecting misformalisations and ensuring the integrity of the conjectures.

[Bhavik Mehta]

I sent this to Pietro already, but since I'm enjoying reading other peoples' abstracts, it's only fair I post my own too:

Title: Formalising Polychromatic Colourings of Integers

Abstract: A colouring of the integers by finitely many colours can be called polychromatic for a finite set S if every translate of S uses every colour. For a fixed number of colours k, it is known that there is a finite bound m(k) for which every set of size at least m(k) admits a polychromatic k-colouring, and a large computer search was used to help prove m(3) = 4. We discuss the (in progress) Lean formalisation of both of these results, which mix topology, probability theory, combinatorics, and software verification, and explore how the philosophy of Lean and mathlib enable this process.

[Jared Duker Lichtman]

Title: Gauss - an agentic formalization of the Prime Number Theorem

Abstact: In this talk we'll highlight some recent formalization advances using a new agent, Gauss. In particular, with Gauss we obtained a Lean proof of the Prime Number Theorem in strong form, completing a challenge set in January 2024 by Alex Kontorovich and Terence Tao. We aim for Gauss to become an assistant for working mathematicians, especially those who do not write formal code themselves.

[Eugenio Cainelli]

We kindly ask all speakers to leave a few minutes for questions at the end of their talks. Also, speakers who use their laptop are encouraged to test their setup before the beginning of each session.

[Sidharth Hariharan]

Title: Formally Packing 8-Dimensional Spheres

Speakers: Maryna Viazovska and Sidharth Hariharan

Abstract: In this talk, we will provide an introduction to the ongoing project to formalise Viazovska's solution to the sphere packing problem in dimension 8. We will share updates on our progress, outline strategies to overcome remaining challenges, and discuss recent AI contributions to our project. Our talk will be based on joint work by Birkbeck, Hariharan, Lee, Ma, Mehta, Viazovska, and community collaborators.