Workshop: Formalization of Mathematics

Monday

Floris van Doorn

William Farmer

Christoph Benzmüller

Tuesday

Kevin Buzzard

Cyril Cohen

Lawrence Paulson

Yves Bertot

Wednesday

Natarajan Shankar

Jacques Carette

Georges Gonthier

Patrick Massot

Thursday

Mohammad Abdulaziz

Florian Rabe

Katja Bercic / Jure Taslak

Johan Commelin

Friday

Jeremy Avigad

Robert Lewis

Claudio Sacerdoti Coen

Wojciech Nawrocki

Mohammad Abdulaziz (King's College London): Formalising the Theory of Combinatorial Optimisation

Combinatorial optimisation is a central area in computer science, applied mathematics, and operational research. Influential ideas and notions developed within the area of combinatorial optimisation include polynomial-time computation, linear programming, flows, and matchings. In this talk I will describe the formalisation, in Isabelle/HOL, of some results from the theory of combinatorial optimisation, with some focus on the theory of matching. I will briefly discuss mathematically interesting findings, some of the mathematical reasoning styles employed there, and potential contributions of formalisations in that area. Joint work with multiple authors.

(Pending permission to publish the recording)

Jeremy Avigad (Carnegie Mellon University): Verifying elliptic curve computations on blockchain

Christoph Benzmüller (University of Bamberg): Comments on the formalisation and automation of foundational theories from the point of view of LogiKEy

Katja Bercic / Jure Taslak (University of Ljubljana): Lean-HoG: Incorporating a database of graphs into a proof assistant

(Pending permission to publish the recording)

Yves Bertot (Inria): Reconciling Type theory with the use of a single type of numbers for mathematical education at introductory levels

I contend that natural numbers are counterproductive in proof assistants, if the objective is to use these proof assistants for teaching math to young students fresh out of high school. In this talk, I explore ways to hide the type of natural numbers from the student’s eyes in mathematical exercises, using only a predicate to describe the corresponding subset of real numbers.

(Pending permission to publish the recording)

Kevin Buzzard (Imperial College London): Capturing mathematical equality

I argue that the decision within the mainstream mathematical community to largely reject constructivism (and in particular not to teach it to first year undergraduates) has led to a confusion about the difference between a theorem and a definition. Mathematicians have attempted to fix this by introducing the ill-defined term “canonical isomorphism” and this phrase is now being over-used in, for example, the number theory literature. This over-use makes my life as a formaliser harder.

(Pending permission to publish the recording)

Jacques Carette (McMaster University): Unavoidable Mathematics

Taking for granted the constructions given to us by Universal Algebra and Category Theory, we can examine what mathematics (and computer science!) arises “for free”. Even very simple theories give rise to a wealth of (known) derived material. Nevertheless, a systematic exploration has never been done. What is surprising is that rather simple theories give rise to scarcely known material..Furthermore mathematics of recent interest (eg: containers, lenses, inhabited spaces) arise naturally. Subtle issues also crop up: Setoids, decidability both make an appearance.In other words, the simplicity is deceptive as a rich tapestry of concepts lies at the “low Kolmogorov complexity” end of theory exploration.

(Pending permission to publish the recording)

Cyril Cohen (Inria): Building Measure Theory using Hierarchy Builder

In this talk I will present the Hierarchy Builder Domain Specific Language for Coq, and illustrate its use in building measure theory and the Lebesgue measure in a concise way. This talk is meant to raise questions that will be relevant for the port of HB to other proofs assistants. Joint work with Reynald Affeldt, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi.

Johan Commelin (Albert–Ludwigs-Universität Freiburg): Condensed Type Theory

Condensed sets form a topos, and hence admit an internal type theory. In this talk I will describe a list of axioms satisfied by this particular type theory. In particular, we will see two predicates on types, that single out a class CHaus of "compact Hausdorff" types and a class ODisc of "overt and discrete" types, respectively. A handful of axioms describe how these classes interact. The resulting type theory is spiritually related Taylor's "Abstract Stone Duality". As an application I will explain that ODisc is naturally a category, and furthermore, every function ODisc - ODisc is automatically functorial. This axiomatic approach to condensed sets, including the functoriality result, are formalized in Lean 4. If time permits, I will comment on some of the techniques that go into the proof. Joint work with Reid Barton.

(Pending permission to publish the recording)

William Farmer (McMaster University): An Alternative Approach to Formal Mathematics that Prioritizes Communication over Certification

(Pending permission to publish the recording)

Georges Gonthier (Inria Saclay Ile de France): Programming Mathematics: Tools and Challenges

Robert Lewis (Brown University): Teaching Lean vs. teaching with Lean

I have taught two courses at Brown University where students have used Lean: one in which formal verification is the subject of the class, and one (in progress) in which the goal is to teach traditional discrete mathematics. I will compare and contrast my approaches in these two settings and ruminate on what has worked and what hasn't.

(Pending permission to publish the recording)

Patrick Massot (Carnegie Mellon University): From informal to formal and back

I will explain tools that help turn informal mathematics into formal mathematics and formal mathematics into informal ones, with the hope that composing those tools leads to better informal mathematics. In particular I will explain how the Lean blueprint infrastructure helps preparing and running a collaborative formalization project, and how it could easily be modified to work with other proof assistants. Then I will talk about my work in progress with Kyle Miller on Informal Lean, a tool that turns Lean statements and proofs into informal mathematics where readers choose the level of details.

Wojciech Nawrocki (Carnegie Mellon University): Extending the Lean user interface with widgets (a tutorial)

Part of the promise of formal mathematics is to improve communication. While this is already achieved to an extent by standardizing statements and clarifying subtleties, visual (for instance geometric) aspects of reasoning are usually lost in communicated formal proofs. Another part of its promise is to prove the obvious automatically; and proof automation can often be better understood by interactively exploring its behaviour. Finally, proof assistants can productively serve as Jupyter-like environments for computing with mathematical data. The Lean 4 editor environment (primarily, but not exclusively, in VSCode) can be extended to accommodate these needs and more. In this tutorial talk, I will demonstrate how to write a simple "widget" visualizing one kind of mathematical object, as well as (time permitting) how to interactively trace the execution of a tactic.

Lawrence Paulson (University of Cambridge): Formalising Advanced Mathematics in Isabelle/HOL

The formalisation of mathematics is now a reality. A number of recent and highly sophisticated papers have been formalised, in some cases before human referees had time to submit their reviews. Most of this work has been done using the Lean proof assistant. The speaker will discuss the accomplishments and conclusions of a six-year research project devoted to formalising advanced mathematics using Isabelle/HOL and highlight some special considerations arising from that choice.

Florian Rabe (University Erlangen-Nuremberg): HOL+Dependent Types + Subtyping

Claudio Sacerdoti Coen (Alma Mater Studiorum - Università di Bologna): A taste of ELPI

Natarajan Shankar (SRI International Computer Science Laboratory): Beautiful Formalizations and Proofs

Beauty in mathematics may or may not be a concept that is formalizable, but beauty is clearly critical for effective formalization. In the context of mechanization of mathematics that has been ongoing over the last four decades, the criterion for beauty needs to be adapted from that of informal mathematics. Beautiful informal arguments might turn out to be less than elegant when formalized, and conversely, the austere beauty of mechanized mathematics might defy conventional standards. In the context of mechanization, particularly the use of decision procedures, a beautiful formalization is one that elegantly leverages the power of formal language and automation to deliver clear, concise, and general definitions and proofs. We illustrate our approach to the aesthetics of formalization with examples.

Floris van Doorn (Universität Bonn): Towards a formalized proof of Carleson's theorem

A fundamental question in Fourier analysis is when the Fourier series converges to the original function. This is true for continuously dierentiable functions, but not always true for continuous functions. In 1966 Lennart Carleson proved that it is true for functions on the real line for almost all points. This follows from the boundedness of the Carleson operator. Carleson's proof is famously hard to read, and there are no known easy proofs of this theorem. Furthermore, generalizations of the theorem to higher dimensions are subtle. Christoph Thiele et al. proved in 2024 a generalized version of the boundedness of the Carleson's operator in doubling metric measure spaces, and I will lead a project to formalize this theorem in Lean. Thiele and his collaborators wrote a detailed blueprint that we will use as the basis for the formalization.