Mathematical libraries of the future

Session of the Academic Advisory Council, Heidelberg University, 26.05.2025.
Florent Schaffhauser, Institute for Mathematics & HEGL Managing Director.

Accessing mathematical literature

• Mathematics is a centuries-old subject, with a vast and heterogeneous literature.
• It takes years of training to explore it, learn how to search and become able to add to it.
• Keeping track of the state-of-the-art is a hard and time-consuming task.
• Access to mathematical knowledge is not equally distributed over the globe.

Digital libraries

• Modern library management systems include databases to index the literature and a public user interface. Textbooks and research articles are sometimes accessible in digital form.
• Is that sufficient to get full and easy access to knowledge? Can we improve on that model?
• In this presentation, we review how the ever-increasing use of computers in mathematical research and higher education is prompting us to enlarge the concept of a mathematical library.
• This also represents an opportunity to bridge the gap with the Global South when it comes to accessing knowledge, but it will take a proactive effort.

Computer-assisted mathematics

We use computers to do mathematics in various different ways:

• Computer algebra systems (CAS) help us perform sophisticated computations.
• Machine learning helps us explore and find patterns in large datasets.
• Interactive theorem provers (ITP) give us a way to represent mathematical concepts as data.

Each of these tools comes with a notion of library, in the sense of software engineering. What does such a library look like in the case of an interactive theorem prover?

What is an Interactive Theorem Prover?

Interactive theorem provers are also called proof assistants and they are built on top of a programming language.

• The language should be powerful enough to encode mathematical concepts in a way that is understandable both by the machine and by the human user, echoing Leibniz's characteristica universalis.
• There is some automation, but the proof/program is still written mostly by the user.

Proof assistants

• The first programming language with such capacities was Automath, implemented by Nicolaas G. De Bruijn in 1967.
• Many others have appeared since: Mizar (1973), Isabelle (1986), Coq (1989), Agda (2007), Lean (2013).
• Created by Leonardo de Moura while working for Microsoft Research, Lean has become quite popular in the mainstream mathematical community in recent years.
• This is due, for a large part, to the existence of a large library of university-level mathematics called Mathlib.

Machine-checked mathematics

• We can formulate mathematical statements in a programming language and have the computer assist us in writing a proof of that statement.
• Mathematical expressions can look just like they would in a textbook.
• The proof assistant tells us when a proof is incorrect or incomplete.

Getting feedback from the proof assistant

• The proof assistant also tells us when the proof is correct and complete.
• Potential applications to higher education are plenty: Exercise sheets, interactive texbooks, etc.
• The challenge is to have libraries of formalised mathematics that we can use at the university level and in research.

The Liquid Tensor Experiment

In 2020, Fields medallist Peter Scholze challenged the Leanprover community to check the correctness of one of his most recent theorems, in the newly-created field of Condensed Mathematics. He did so via a blog post. Only 18 months later, the challenge was completed. The findings of the project became the topic of an article in Nature.

Definition 1. Condensed sets are sheaves on the pro-étale site of a point.

The Freiman–Ruzsa conjecture

In 2023, another fields medallist, Terence Tao, took an interest in Lean and used it to formalise the proof of one of his most recent papers.

In just 6 months, the project was completed: The proof-checking process took less time than the refereeing process of the corresponding article.

Impact on mathematical research

These formalisation challenges were met due to a conjunction of factors that have become characteristic of the field and are reshaping modern research in mathematics:

• A large-scale collaboration (>20 experts, dozens more contributors).
• The development of a new infrastructure, with research happening mostly online.
• The use of a research-level library of formalised mathematics called Mathlib.

Mathlib

• Lean's major mathematical library, called Mathlib, became prominent with Lean 3 (2017-2021). It was ported to Lean 4 in 2023.
• At the time of writing, Mathlib boasts:
  • 103,041 definitions and 205,699 theorems.
  • 556 contributors.
  • 28 expert maintainers (mathematicians and computer scientists).
• Discussion around Mathlib development occurs on the Leanprover Zulip channel. Most of it is public. The code is open-source and freely available on GitHub.

Mathematics as data

Fermat's Last Theorem

• The most emblematic ongoing project in the Leanprover community is the formalisation of Fermat's Last Theorem, led by Kevin Buzzard (Imperial College).
• It is funded by a 5-year EPSRC grant (2024-2029, British Research Council).
• It is an open-source, large-scale, collaborative project, whose progress towards completion can be followed live online, via a tool called Lean Blueprint.

Impact on mathematical education

• Students can experiment with mathematics. They get feedback on their proof and can see where their strategy fails or what is missing.
• Students can collaborate to ongoing research starting at an early stage of their curriculum.
• Students develop new programming skills, making them more competitive on the job market after graduating.
• The distance with real-world applications is getting shorter: Mathlib is written for research, but chunks of it have been used in software verification and optimization, e.g. in cryptography or differential privacy.

Initiatives in Heidelberg

• Heidelberg University has a relatively large group of Faculty members interested in Lean, working in different mathematical fields but all interested in formalisation:
  • Prof. Dr. Judith Ludwig (Automorphic forms and -adic geometry).
  • Dr. Florent Schaffhauser (Complex geometry).
  • Dr. Denis Vogel (Algebra).
  • Dr. Junyan Xu (postdoctoral researcher in Prof. Ludwig's group).
• We run a Research seminar on Formal Mathematics (created in 2024).
• We are developing a Heidelberg Lean Library, for the usage and training of students.

Research-oriented teaching

• The Computer-assisted mathematics student seminar was created in 2023. It runs every year. Three Bachelor theses have already emerged from it. More will follow soon.
• The Heidelberg Experimental Geometry Lab (HEGL) has created a Heidelberg Lean Game to introduce more students to Lean. Our initiative will be the topic of an article in the Bulletin of the German Mathematical Society (DMV).
• Dr. Vogel is formalising his and Dr. Kasten's book on the Foundations of Plane Geometry.
• F.S. has given lectures on Interactive Theorem Proving in Lean for young resarchers, at the Heidelberg Graduate School (MathComp) and at the Max Planck Institute for Mathematics in the Sciences in Leipzig.

Contributions to research

• Prof. Ludwig has a recent preprint on the formalisation of the Bruhat-Tits tree.
• Dr. Xu is a prominent Mathlib contributor, currenlty involved in the formalisation of Fermat's Last Theorem.
• Prof. Ludwig and F.S. have also contributed to Mathlib.

An area of active interdisciplinary research

• Mathematical software libraries are shaping the future of our discipline.
• Interactive Theorem Provers will keep improving and gain traction.
• We aspire to keep expanding and make Heidelberg University a leader in the field.

Discussion panel: A shift in mathematics?