FMM 2021 – Fifth Workshop on Formal Mathematics for Mathematicians

30–31 July 2021

The FMM workshop series enables mathematicians interested in computer assistance and researchers in formal and computer-understandable mathematics to meet and exchange ideas. The meeting provides a platform for discussion of suitable forms of computer assistance between the formal community and interested mathematicians and other researchers.

The main points of interest include

• formalization of challenging mathematical problems
• design of proof languages and techniques
• repositories of formalized mathematics
• interactive and automated theorem proving
• development of proof assistants
• semantic representation of mathematical knowledge
• formal tools in program verification
• foundations and philosophy of mathematics
• proof assistants in education

Invited speakers:

Manuel Eberl, TU Munich, Germany

​Title: Fighting the Curse of De Bruijn

​Abstract: Everyone who ever formalised an informal pen-and-paper proof is familiar with the annoying fact that the formal proof tends to be several times lengthier, more detailed, and more painful than the original informal one. In the first half of this talk I will present some of my thoughts on what contributes to this, and specific examples of how the problem can be (and successfully been) mitigated in Isabelle/HOL. In the second half, I will talk more concretely about one particularly striking example: a domain-specific automation tool to solve problems related to the asymptotics of real-valued functions.

Mario Carneiro, Carnegie Mellon University, USA

​Title: Porting Mathlib

​Abstract: The mathlib library is over 600K lines of code, all written in Lean 3. Lean 4 promises great extensibility, faster tactics, powerful and convenient macro programming – and no backward compatibility. As we have no desire to part with such a rich source of advanced formal mathematics, we are planning to port all of it to Lean 4. This might be the largest source-porting effort done in a theorem prover, so we're taking things slowly and investing heavily in high quality automated porting tool development. In this talk I will discuss our plans for how to translate all this source code to Lean 4 while preserving the quality standards and synthesizing the styles and tactics developed in mathlib with the new Lean 4 style.

List of accepted papers

Programme

See FMM sessions in the CICM programme on Friday, July 30 and Saturday, July 31.

Submissions

Electronic submission is continuous and done via EasyChair: select the author role, select the "new submission" tab, and choose FMM. We welcome submission of short papers presenting research related to the workshop's points of interest. Submitted papers should be 4–6 pages long and formatted in LaTeX using the style onecolceurws (the corresponding style files can be downloaded from here).

• Submission is continuous until 14 July 2021 (AoE).
• Reviews sent back no later than 21 July 2021.
• Final revised papers due by 25 July 2021.

At least one author of each accepted paper is expected to attend FMM and present the work online.

We plan to publish electronic proceedings in the CEUR Workshop Proceedings series.

Organizers and Programme Committee

• Mauricio Ayala Rincón, Brasilia University, Brasil
• Jasmin Blanchette, Vrije Universiteit Amsterdam, the Netherlands (co-chair)
• Anthony Bordg, Cambridge University, UK
• Johan Commelin, Universität Freiburg, Germany
• Sander Dahmen, Vrije Universiteit Amsterdam, the Netherlands
• Adam Naumowicz, University of Bialystok, Poland (co-chair)
• Karol Pąk, University of Bialystok, Poland