| Speaker |
Title |
Abstract |
| David Roe |
LMFDB: Past, Present and Future |
I will provide an introduction to the LMFDB in its current state, aimed at participants who have not used it much, if at all. I will then discuss the ways in which the LMFDB is adapting to large language models and formalization and the role that I think mathematical databases will play in in the age of AI. |
| Paul Lezeau |
Fantastic (Formal) Proofs and How to Write Them |
The goal of this talk is to give an intro to Lean for people who aren't too familiar with it. After covering some of the basics, I'll also talk a little about how to use AI tools to assist with formalisation. |
| Riccardo Brasca |
Number Theory in Mathlib |
In this talk, I will explain how to work with the standard number-theoretic objects available in mathlib, such as number fields, ideal decomposition, class groups etc. Through concrete examples, I will 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. |
| Kevin Buzzard |
Number Theory and FLT |
I'll go through the results in LMFDB-related areas that I'll need to formalize FLT, and say something about their current status. |
| Junyan Xu |
Elliptic Curves in Lean |
I'll introduce the implementation of elliptic curves in mathlib in terms of Weierstrass equations, and basic constructions like the coordinate ring, the function field, and the group of rational points. As an example, I'll show how certain theorems and conjectures about ranks of elliptic curves are stated in Lean. Along the way I'll mention aspects of my joint mathematical and formalization work with David Ang concerning associativity of group law, elliptic divisibility sequences and division polynomials, bilinear forms underlying projective addition formulas, and reduction homomorphism and group scheme structure, including some open questions. |
| David Loeffler |
Modular Forms in Mathlib |
I will give an overview of the theory of modular forms as currently implemented in Mathlib, focussing on some of the places where the formalizations differ from standard textbook approaches. I'll also survey some of the aspects of the theory that are not implemented yet but are within relatively easy reach, and what is needed in order to get these into the library. |
| Alain Chavarri Villarello |
Formally Certifying LMFDB Number Field Data |
Key invariants of number fields have been extensively computed using computer algebra systems and collected in databases such as the LMFDB. While these systems are efficient, their output is not formally verified. To bridge this gap, and to make some of these data available for use in future formalized proofs, we have developed certificates in Lean 4 built around data types amenable to computation. In this talk, I will focus in particular on certifying rings of integers and class groups of number fields in Lean, together with related invariants such as discriminants, signatures, and unit groups modulo p-th powers. Using these methods, we formally verified hundreds of LMFDB entries. This talk contains joint work with Anne Baanen and Sander Dahmen. |
| Richard Hill |
Local Class Field Theory and Continuous Cohomology |
Last summer there was a workshop on formalizing local class field theory. I will explain the approach taken there and the progress made (see https://github.com/kbuzzard/ClassFieldTheory). I'll then discuss the difficulties of restating the main results in terms of continuous cohomology rather than abstract group cohomology. I'll show some API designed to make this translation possible. |
| Bhavik Mehta |
Metaprogramming in Lean |
One activity at this workshop will be to brainstorm tools (broadly construed) that will help with the formalization of aspects of the LMFDB. Tools are not themselves formal proofs in Lean; often they take the form of metaprograms, pieces of code that interact with Lean expressions in various ways. Tactics are the most familiar kind of metaprogram to most Lean users. In this talk I will introduce the basic components of a Lean metaprogram and describe different tactic design strategies, including proof by reflection and proof by certificate. Better understanding of the basic building blocks of Lean tooling will help brainstorm new ideas and applications. |
| Katerina Hristova, David Ledvinka, Justus Springer |
Formal Landmarks - A Dataset of Modern Formalized Theorem Statements |
We describe our efforts to build a public dataset of formalized statements of recent theorems from the Annals of Mathematics. In doing so, we address a lack of formalization at the frontier of mathematical research and expand Mathlib by adding missing definitions and theorems. Our project aims to provide clear targets for AI systems on a wide range of tasks, including auto-formalizing proofs and assisting humans in proof formalization. |
| Xindi Yang |
Formalization of Noga Alon's Combinatorial Nullstellensatz (1996) |
We formalize Noga Alon's Combinatorial Nullstellensatz (1996) in Lean 4, generating approximately 2,500 lines of verified code. Pure LLM produced the Lean definitions and statements from the original paper's natural-language proof; human then refined portions of the code through dialogue with the LLMs, leaving sorry placeholders for Aristotle, a cloud-based automated prover, to close via API. We explicitly exclude later generalizations (e.g., Alon's 1999 extension) to faithfully reflect Alon's original proof, also we do not use interactive tooling or specialized coding agents. |
| Barinder Banwait |
A Formal Proof of the Ramanujan--Nagell Theorem in Lean |
The Ramanujan--Nagell theorem is that there are only 10 solutions in integers to the exponential Diophantine equation x^2 + 7 = 2^n, namely those with n = 3, 4, 5, 7, 15. I'll talk about a formalization of the proof of this theorem in Lean, highlighting in particular the QuadraticAlgebra structure. |
| Wenrong Zou |
Formalization of Formal Group Laws |
In this talk I will discuss the formalization of one-dimensional formal group laws in Lean. I will explain how a commutative formal group law induces an AddCommGroup instance on the (multivariate) power series with nilpotent constant coefficient. I then describe the formalization of homomorphisms and isomorphisms of formal group laws, and show how an isomorphism induces an additive group isomorphism between the associated groups. |
| William Coram |
Newton Polygons |
Newton polygons are a graphical construction we can attach to a power series, they consist of a sequence of connected segments and the slopes of which allow us to gather information on zeros of the power series. However, since they are of a graphical nature, deciding on a general enough definition has posed a challenge. In this talk we will discuss the progress made on giving a definition that works for various applications, as well as the formalisation of an algorithm that will allow us to attach something of type "newton polygon" to a power series. |
| Thomas Browning |
Constructing L-Functions in Lean |
I will discuss the infrastructure recently added to mathlib for defining L-functions, and some of the design decisions that were made. |
| Drew Morris |
Formally Verified Categorical Diagram Serialization |
The hallmark tool in category theory is diagrams, which are very visual in nature. These diagrams represent category theoretic properties cleanly, intuitively, and expressively. However, due to their visual nature, they are difficult to represent in Lean. I am developing a data serialization pipeline through multiple equivalent representations of categorical diagrams. This would allow one to reason about categorical diagrams in a GUI (the medium of choice) while producing Lean theorem statements and proofs (the deliverable of choice). |
| Andrew Yang |
TBD |
TBD |
| Xavier Roblot |
Formalization of the Analytic Class Number Formula in Mathlib |
We present a complete formalization of the Analytic Class Number Formula in Mathlib. We outline the main steps of the proof: lattice point counting, volume computation, and Abel summation, and discuss some of the challenges encountered during the formalization. |
and the 