Universität Bonn

Workshop: Formalization of Mathematics

This workshop is devoted to the central theme of the Trimester: How do current and future developments of Formal Mathematics impact and assist active research in central areas of pure mathematics. Talks will focus on examples of such interactions, as well as on the development of adequate techniques. Some half-days will be reserved for informal demonstrations, collaborations and co-working.

Federico Zerbini (University of Oxford): Conical Sums

Conical sums are periods defined by certain infinite sums over lattice points contained in cones of n. Special cases include multiple zeta values, as well as Matsumoto-Witten zeta values associated with semisimple Lie algebras. They have also appeared in the computation of string theory amplitudes. The \mathrm{ab}-algebra generated by conical sums was proven by Terasoma to coincide with the ab-algebra of cyclotomic multiple zeta values; all relations in this algebra are conjectured to follow from decompositions of cones. Open questions on Matsumoto-Witten zeta values would be answered by proving a general conjecture of Dupont about the motivic nature of conical sums. I will introduce conical sums and their algebra, and report on the current state of the art on Dupont's conjecture.

Mohammad Abdulaziz: Formalising the Theory of Combinatorial Optimisation

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

Jeremy Avigad: 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

Christoph Benzmüller: 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

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

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)

Video not found

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.

Kevin Buzzard: Capturing mathematical equality

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.

Jaques Carette: Unavoidable Mathematics

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.

Cyril Cohen: Building Measure Theory using Hierarchy Builder

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.

Johan Commelin: Condensed Type Theory

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

William Farmer: An Alternative Approach to Formal Mathematics that Prioritizes Communication over Certification

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

Georges Gonthier: 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)

Video not found

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.

Patrick Massot: From informal to formal and back

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.

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

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.

Lawrence Paulson: Formalising Advanced Mathematics in Isabelle/HOL

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

Florian Rabe: HOL+Dependent Types + Subtyping

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

Claudio Sacerdoti Coen: 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.

Natarajan Shankar: Beautiful Formalizations and Proofs

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.

Floris an Doorn: Towards a formalized proof of Carleson's theorem

Panel Discussion on Formalization in Mathematics

Moderation: Josef Urban

Panel Discussion on Formalization in Mathematics

Wird geladen