How to Build a Formal Mathematical Library in which Communication is
Prioritized over Certification: An Extended Abstract

William M. Farmer

2026

Abstract

Formal mathematics is mathematics done within the framework of a
formal logic.  The standard approach to formal mathematics, in which
mathematics is done with a proof assistant and all details are
formally proved and mechanically checked, focuses on certification.
In contrast, the free approach to formal mathematics, an alternative
to the standard approach that is free of the obligation to formally
prove and mechanically check all details using a proof assistant,
focuses on communication and accessibility.  A formal mathematical
library (FML) is a repository of mathematical knowledge expressed
within a formal logic and organized as a network of interconnected
axiomatic theories.  This talk presents the free approach, describes
how a communication-oriented FML can be built using the free approach,
and ends by encouraging the mathematics software community to develop
the logics and software needed to build communication-oriented FMLs.